Closed caobo1994 closed 4 years ago
I agree with @caobo1994. In particular, you make use of relational operators (<, <=, etc), but you do not define their meaning. You need to define what a day is to define these operations.
Right, so DayT comes from the Day ADT Module. And DayT is a tuple of (Natural Number, Natural Number, Natural Number) But for the ADT Module. Its exported type is DayT = ? So I don't know where should I put the formal definition of DayT
@sharyuwu, an ADT should be exported as ?. You just need to give access programs that allow users to inspect the value. Since you have comparisons, you'll want the ADT to export functions for <, <= etc.
@sharyuwu Not necessarily. You can simply say that Day1<Day2 means Day1 is before Day2, and similar meanings for other operators.
@smiths Right, I think I got what you mean. SO can I name the exported Access program as symbols like <, <= in this document? @caobo1994 I think Doctor smith feels creat extra functions for it can make it more explicit
I still prefer defining operators (called 'operator overloading' in some programming languages). First, you give a plain information about the meaning of each operator, then you give a formal mathematical definition of the operator by comparing the members of DayT.
In addition, you only need to define one operator '<' in detail, since there are default definitions of other operators from this operator.
@caobo1994 But where will be the proper place to write this operator's information? In Assumption maybe?
Define operators like functions. Try define operator< (day1, day2)
sharyuwu notifications@github.com 于 2019年12月4日周三 18:09写道:
@caobo1994 https://github.com/caobo1994 But where will be the proper place to write this operator's information? In Assumption maybe?
— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/sharyuwu/optimum-tilt-of-solar-panels/issues/51?email_source=notifications&email_token=AEJS27IF3ZMTQ2DFRBSMS33QXA2B5A5CNFSM4JVQENJKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEF62N4I#issuecomment-561882865, or unsubscribe https://github.com/notifications/unsubscribe-auth/AEJS27OP2PB4WCT6L7DNYCDQXA2B5ANCNFSM4JVQENJA .
Yes, @sharyuwu, you can name an access program with the symbol <. It is an infix symbol, but by the definition of the semantics below, the reader will know how to interpret it. You can then explain, in the semantics portion how the DayT argument is compared to self (the current object) to determine a truth value.
You don't even have to define this with words. There are some math formulas for calculating dates as the number of days from a specific date. You can then use regular arithmetic to calculate the difference. After a quick google search, I found this link:
@caobo1994 Yes, I think you and Dr. Smith are aiming the same page:) @smiths Thank you for the website and the explanation. So if I use the math formulas to represent my DayT, can the statement variable for storing the DayT represent in Integer, like day : Integer?
@sharyuwu, I recommend that you use a natural number for the day, since there won't be any dates that are negative numbers. You could even define a new type that will only take values between 1 and 31, but you don't need to go that far. :-)
My advice would be to have the state variables for DayT inside the DayT ADT. I don't think you really need a separate type that is a tuple of the data. The data and the behaviour make more sense together.
@caobo1994 @smiths I add the function definition regarding operator functions <=, <. Then remove the function compare. See the changed line in https://github.com/sharyuwu/optimum-tilt-of-solar-panels/commit/48be4e50631134c57ea767521ed7946f14a10806#diff-b1bd046f21124a53c1bb4ef387323431L329-R333 Here is how I define the functions.
Please give me some feedback on the changed! I will close this issue for now because the change was made.
You have not give a formal definition of DayT, including its members, types and meanings.