Homework 1 Notes

The following is a set of notes, written by Tao and lightly edited by David, that describe a set of problems and issues that arose during grading of the first homework. They are not complete descriptions of how grading was done, but they (among other things) point out a few common problems.

Reminder: if you have questions about the grading on your assignment, first get in touch with Tao for clarification; if you still feel there are issues to be resolved, then get in touch with David.

1. Program correctness (40 points, 10 points each)

• a) & b) David mentioned following approach in class mail list: For each assignment statement, you’ll need to use the {Q(E)} x := E {Q(x)} definition of assignment. Some students used this approach, but many were not careful about the correspondence between E and x in Q(E) and Q(x). For example, consider:
  
  {true}
  max := x
  {((max = x) or (max = y)) and ((max >= x) and (max >=y))}
  
  For this:
  
  Q(E) º (((x = x) or (x = y) and ((x >= x) and (x >= y))),
  Q(x) º (((max = x) or (max = y)) and
  ((max >= x) and (max >= y))).
  
  In fact, since max := x (like x := E), the correct form should actually be
  
  Q(x) º (((x = x) or (x = y) and ((x >= x) and (x >= y))),
  Q(max) º (((max = x) or (max = y)) and
  ((max >= x) and (max >= y))).
  
  
• You could use {Q(E)} x := E {Q(x)} or the following weakest precondition theorem in proof:
  Theorem:
     Any triple of the form {Pw}S{Q} is valid if Pw is the weakest precondition of Q. More generally, the triple {P}S{Q} is valid if and only if P implies Pw.
  (Thanks to Christina Cyr for providing the following links in her homework solution.) http://www.google.com/search?q=cache:www.middlebury.edu/classes/fall97/learn_assertions/weakestprec.html+Hoare+triples,+Weakest+Precondition&hl=ja
  
  
• You could view following materials to know more about program proofs. (Thanks again to Christina for providing these links.)
• http://www.cs.caltech.edu/~cs138/1997-98/138a/notes.html : Prof. K. Mani Chandy’s Sequential Program course materials. You could review the first part: Specifications, Reasoning, and Computational Complexity and the first section of second part: Lecture Notes on Iteration.
• Several proof examples of program correctness:
  http://www.cs.unc.edu/~stotts/COMP204/senotes/proof1/main.html
  http://www.cs.unc.edu/~stotts/COMP204/senotes/proof2/main.html
  http://www.cs.unc.edu/~stotts/COMP204/senotes/proof3/main.html
  http://www.cs.unc.edu/~stotts/COMP204/senotes/proof4/main.html
  http://www.cs.unc.edu/~stotts/COMP204/senotes/proof5/main.html
  
  
• c) Some students only gave the “partial” loop invariants. That is, you found invariants that are true but not sufficient to prove the desired postcondition for the loop. It isn’t possible to verify whether you have found the complete loop invariant, except by whether it allows one to prove that postcondition.
  
  Tao says: In theory, to get the complete loop invariant, you could list all the possible invariants and then check whether the program satisfies these possible invariants. Or starting from those predicates in the program, try to derive all possible predicates. However, you may encounter problems by doing so. First, how to define “complete”? If you have “x=y” in your invariants, shall I add “x=y*1” or “x=y-1” into invariants to make it complete. OK, you may leave out those predicates that could be derived from only one invariant. Then in our problem, if in the precondition I limit us to “x>0”, shall I include “y<=z<= x*y” to make it complete? Now this new predicate is derived from both “{1 <= n <= y} AND {z = x * (y – n + 1)}”. Ultimately, we could say that there are infinitely many potential invariants that could be reported. In fact, less strong loop invariant “{1 <= n} AND {z = x * (y – n + 1)}” could be sufficient to prove the postcondition according following theorem David mentioned in class. But you could not prove it with only {z = x * (y – n + 1)}:
  
  If we have {P} while B do S {Q} then find I such that
  – P => I -Invariant is correct on entry
  – {B ∧I} S {I} –It’s invariant
  – {~B ∧I} => Q –Loop termination proves Q
  
  FYI: Although invariants are difficult to discover by naked eyes, they are quite useful in many aspects of program development. David and his former Ph.D. student Michael Ernst did some great research in program invariant detection and developed a tool – Daikon to help discovering program invariants. If you are interested, please visit: http://sdg.lcs.mit.edu/~mernst//daikon/
  
  
• d) Most students didn’t get the correct solutions to this question.
  
  
• Some students may come out with the question of “ What is aspecification?” when solving this problem. You could find an uses-requires-modifies-ensures notation from Prof. Chandy’s course materials (http://www.cs.caltech.edu/~cs138/1997-98/138a/notes/spec/spec_notation.ps ). More simply, you could just assume specification is composed of the precondition and postcondition.
  
  
• You are not allowed to make your precondition TOO STRONG, because by doing so, you may refuse those reasonable inputs!!!! But I was generous in tolerating preconditions that were too weak, because by giving this too weak specification, you can still handle those error inputs such as “0³b² – 4ac” (assuming you don’t allow imaginary root”) in your implementation.
  
  
• Let’s come to general case, if you give a TOO STRONG precondition specification, you are giving a WRONG specification!!! But if you give a too weak precondition specification, it may not be classified as wrong specification, maybe we could say this specification didn’t capture all those aspects of problem completely, say, didn’t consider those error input, let’s recall the robust version in Z document. It is tolerable, since we could refine it to a better (robust) specification, just like adding some more limitations on specification or just add some codes in implementation to handle those error inputs.
  
  
• In the postcondition, some students only specify “{A*x² + B*x + C=0}”, from first thought, you may think it is acceptable, indeed it tells the truth that all those x values which satisfy the equation could be the roots. However, you ONLY get ONE solution, not all the solutions. Many students specify the postcondition as “{A*x1² + B*x1 + C=0}^{A*x2² + B*x2 + C=0}, it seems correct too, however, it is also WRONG. I will simply give you a wrong implementation as “x1 = (-B + sqrt(B*B – 4AC))/2A); x2 = (-B + sqrt(B*B – 4AC))/2A)”, you only could get one root. Please see correct solution we post in solution webpage.
  
  
• “AND” or “OR” in postcondition. The post-condition could be {A*x1^2 + B*x1 + C = 0 and A*x2^2 + B*x2 + C = 0) and …..} V …, but not “or” to connect them. If you use “or”, assume you use {(A*x1^2 + B*x1 + C = 0 or A*x2^2 + B*x2 + C = 0) and …..} V …, then how about a program which implements this spec with A*x1^2 + B*x1 + C = 0, but x2= any value?
  
  
• Hint: Most students write down both the implementation and specification (precondition and postcondition). Indeed you could use the techniques in 1) Program Correction to prove successfully the postcondition from the implementation you provides. But you may not notice that another WRONG implementation also could satisfy your postcondition!!! So in order to inspect whether you get a correct specification, try to remove the implementation and imagine those possible incorrect implementations which satisfy your postcondition. If you could come out one of them, then you know you get a wrong specification.

2)  Z (40 points total)

· a.

o If you explain the reason as “not making an assignment”, not mentioning “not limiting other elements in the birthday set”, you will lose 5 points for that. In fact, “not making an assignment” is not the problem. Please notice the postcondition has no responsibility to make assignments for any new entities appearing in postcondition. For example, {true}……{x>0}.

o What postcondition doesn’t specify is “unknown”, NOT “false”! For example, new postcondition “{name? |®date?} Î birthday'” only specify the fact “it should include the new name/date pair”, not “it ONLY include the new name/date pair”. Indeed, in some proof system (such as some in AI), what is not specified in the system could be considered as FALSE, however, here you are not allowed to assume so.

· b.

o You could answer this question using two approaches. One is to decompose DATE atomic element into YEAR, MONTH, DAY atomic elements. The other is to map the DATE atomic element to certain sequence number. Either way will allow for operations, such as distinguishing earlier and later dates, determining the difference between two dates, and any other operations you wish in this general style. 

· c.

o In v) and vi), some students misunderstand the “robust” version. “Robust” version is not a version which implements more functionalities, but a version could handle those inputs which include mistakes, please see Z document 1.3 page 7.

o You are not expected to modify the original specs to make it robust, please refer to Z document 1.3 page 7, “modifying it to describe the handling of incorrect input could only make it obscure”.

o Some students only list those additional operations to handle the error input, but don’t specify the specification for the robust version of operation, which combines the original operation and error handling operations.

3. Finite state specifications (40 points)

· You are expected to capture satisfactorily enough details of the system. A few students just describe the system too simply. To assume you present your statechart to implementers, they will feel rather confused on “how to do”, because you don’t give them enough “what to do” information.

· “Use Parallel States (AND decomposition)!!”, in fact, in this system, many states transition could be performed in parallel. It is hard to describe this feature without using parallel states David introduced in class.

· It is recommended to use the hierarchical structure to control the complexity, but not strictly required. If your statechart contains too many states, maybe you could consider to compress some closely related states into one high-level state and draw another statechart which contains those states it is decomposed to. If you use this technique, be cautious to make the consistence between high level state and low level corresponding statechart. I mean, they are supposed to have the same “arrow-in” and “arrow-out”.

· Each top level parallel state should have start point. A few students’ statecharts don’t have a start state, and this is a problem.

· A few students confused states and transitions (event). You should be careful about this. For example, in the spec, a few students specify “Play Now” as a state, in fact, it is a transition or event. Indeed, you could enter “Playing game” state after you click the “Play Now” button (“Play Now” transition or event). It is preferable to distinguish the state and transition by giving state some noun phrases and transition some verb phrase.

· A few students draw their statecharts just like flow chart. They include condition diamond in their statecharts. Actually you could decompose the conditional transition into several individual transitions by specifying their conditions in their names. There are still some differences between flow chart and statechart. Maybe students could discuss this in our course mail list?

· When to decompose one state to several states and when not ( I just come out with following two principles, you may come out more):
Internal transition requirement: Just considering the checkbox option, assume when it is check on, you are only allowed to check off, vice versa, then you will have to draw two states for check on state and check off state separately to limit the transitions between them.
External transition requirement: Considering the checkbox option, if other states’ transitions depend on which state the system is between check on and check off, for instance, in the cassette tape recorder example David gave in class, you need to decompose the check on/off to two different states.

FYI: In David’s cassette tape recorder example, maybe you would notice the volume control only have one state, different from other option buttons. I guess there are two possible reasons, one is that volume is not easy to quantified. Most importantly the other reason is other state transitions don’t depend on the volume states (how high the volume is). As you may know, some SONY tape recorders have a volume protection option button, if you turn it on, even when you turn the volume up to maximum, the volume sound is still not very high in order to protect your ear from harm. For this type of tape recorder, you may decompose the volume state to several states. You could try it!

· When there are some interactions between different parallel states, for example, in David’s cassette tape recorder example, many state transitions use the option states. In these cases, you may use some internal events to coordinate these parallel states.

· “Don’t let your system get stuck in a ‘dead state’ in your statechart!!”, in some cases, a few students just use one transition to enter certain state which has no transition to other states. These “dead states” are not supposed to be quite common in statechart. So after you finish your statechart to check whether your statechart has dead state and whether your system really should be stuck there or it is your mistake.

· You’d better mark the notations, I mean, names for each transition and state if possible.

4) Miscellaneous (30 points total, 10 points each)
a.

· You are required to pick up those properties your spec has. You are not supposed to specify the properties which could not be checked with model checking using YOUR checker specification.

· Be careful that model checker is not “magic”, it could only check some properties based on your specs. It only knows the knowledge presented in spec you wrote. So you are supposed to give some concrete properties specific for your spec.