# 6.894 Lightweight Formal Methods - Problem Sets ^af4f23 ## Metadata **Created**:: [[2025-04-27]] **Host**:: [[groups.csail.mit.edu]] **Source**:: #from/clipper **Status**:: #x **Title**:: 6.894: psets **URL**:: [groups.csail.mit.edu](https://groups.csail.mit.edu/sdg/6.894/problemsets.html) **Zettel**:: #zettel/fleeting **Tags**:: #formal-method ## Calendar [6.894: calendar](https://groups.csail.mit.edu/sdg/6.894/calendar.html) ## Reading A [Reading A](https://groups.csail.mit.edu/sdg/6.894/assignments/readingA.html) - Introductory Flames *(due Mon Feb 7)* - [sample solutions](https://groups.csail.mit.edu/sdg/6.894/assignments/readingAsoln.txt) 1. [Jonathan Jacky](http://staff.washington.edu/~jon/). *The Way of Z: Practical Programming with Formal Methods*. [Cambridge University Press](http://www.cup.org/), 1997. ISBN 0-521-55976-6 (pbk), ISBN 0-521-55041-6 (hbk). Website: [http://staff.washington.edu/~jon/z-book/](http://staff.washington.edu/~jon/z-book/) 2. Susan Lammers. *Programmers at work : interviews with 19 programmers who shaped the computer industry*. Chapter: Butler Lampson. Redmond, WA: [Tempus Books of Microsoft Press](http://www.edv-buchversand.de/mspress/index.asp), 1989. ISBN: 1556152116 3. C. A. Hoare. *The 1980 [ACM Turing Award Lecture](http://www.informatik.uni-trier.de/~ley/db/journals/cacm/turing.html)*. Delivered at ACM '80, Nashville, Tennessee, October 27, 1980. 4. Anthony Hall and Roderick Chapman. *Correctness By Construction: Developing a Commercial Secure System*. IEEE Software. Jan-Feb 2002. 5. M. Jackson, "Brilliance", from *Software Requirements And Specifications*, [Addison-Wesley Addison Wesley Professional](http://www.awprofessional.com/index.asp), 1995. ### Study Questions A Be concise, clear, and thoughtful; for most questions, a sentence of two should suffice. There is more than one right answer and more than one wrong answer. 1. What does Jacky say is the only role for testing? Do you agree? 2. How does Lampson describe a "beautiful program"? Does this sound right to you? 3. What feature of Algol 60 excited Hoare and why? For Hoare, what is the higher goal of programming language design? Which of his comments look dated and which have stood the test of time? Give one example of each. 4. Is Hall's analogy between software and cars appropriate? Does Hall think that construction-by-correctness can eliminate all defects? 5. It is quite possible that Fred's project was fundamentally complex and Jane's was not. As a manager, how would you evaluate the quality of their work? ## Problem Set 0 [Problem Set 0](https://groups.csail.mit.edu/sdg/6.894/assignments/ps0.html) - Relational Logic Exercises *(due Mon Feb 14)* - [sample solutions](https://groups.csail.mit.edu/sdg/6.894/assignments/ps0soln.txt) [PDF](https://groups.csail.mit.edu/sdg/6.894/assignments/ps0.pdf) ## Problem Set 1 - [Problem Set 1](https://groups.csail.mit.edu/sdg/6.894/assignments/ps1.html) - Simple Alloy Models *(due Tue Feb 22)* - sample solutions: [#1-3](https://groups.csail.mit.edu/sdg/6.894/assignments/ps1soln.txt), [#4](https://groups.csail.mit.edu/sdg/6.894/assignments/lmendelPS1/4.html) [PDF](https://groups.csail.mit.edu/sdg/6.894/assignments/ps1.pdf) ## Reading B [Reading B](https://groups.csail.mit.edu/sdg/6.894/assignments/readingB.html) - Formal Methods and Software Design: Advocacy and Critique *(due Mon Feb 28)* - [sample solutions](https://groups.csail.mit.edu/sdg/6.894/assignments/readingBsoln.txt) 1. Brian Cantwell Smith. *The Limits of Correctness*. ACM SIGCAS Computers and Society. NY: ACM Press, 1985. 2. Anthony Hall (Praxis Systems). *Seven Myths of Formal Methods*. IEEE Software, 7(5): 11-19, Sept. 1990. 3. Michael Jackson. Formal Methods and Traditional Engineering. Journal of Systems and Software. Special issue on Formal Methods Technology Transfer. Volume 40, Number 3, pages 191-194, March 1998. 4. C. A. Hoare. *Essays in Computing Science: Programming is an Engineering Profession*. Chapter 18. [C. B. Jones](http://homepages.cs.ncl.ac.uk/cliff.jones/home.formal/) (editor). Upper Saddle River, NJ.: [Prentice-Hall](http://www.phptr.com/), 1989. Website: [http://portal.acm.org/citation.cfm?id=63445](http://portal.acm.org/citation.cfm?id=63445) 5. John Rushby. *Calculating with Requirements*. 3rd IEEE International Syumposium on Requirements Engineering. Annapolis, MD, January, 1997. IEEE Computer Socicety Press, pp 144-146. 6. [Frederick P. Brooks, Jr.](http://www.cs.unc.edu/~brooks/). *The Mythical Man Month*. Reading, MA: [Addison-Wesley](http://www.awprofessional.com/index.asp), 1995. 7. [Kent Beck](http://c2.com/ppr/about/author/kent.html). *Extreme Programming Explained: Embrace Change*. [Addison-Wesley](http://www.awprofessional.com/index.asp), 2000. ISBN: 0-201-61641-6 Website: [http://www.awprofessional.com/titles/0-201-61641-6](http://www.awprofessional.com/titles/0-201-61641-6) 8. Matt Stephens and [Doug Rosenberg](http://c2.com/cgi/wiki?DougRosenberg). *The Case Against XP*. [Apress](http://www.apress.com/), 2003. ISBN 1-5905-9096-1 Website: [http://www.apress.com/book/bookDisplay.html?bID=150](http://www.apress.com/book/bookDisplay.html?bID=150) ### Study Questions B Be concise, clear, and thoughtful; a short paragraph should usually suffice. Tell us what you really think. There is more than one right answer (but also more than one wrong answer). 1. Brian Cantwell Smith ends the first section with this bold statement: Just because a program is "proven correct", in other words, you cannot be sure that it will do what you intend. Choose one of the 4 points Smith introduces in the following section (complexity, human interaction, levels of failure, correctness and intention) and discuss how it can be used to argue both against and in favor of the use of incomplete/partial models. 2. Choose one or two of Anthony Hall's 7 points and discuss how your own experiences (not just what you have been taught) support or diverge from his conclusions. 3. What does Michael Jackson means when he says Specialisation is the inevitable precondition and accompaniment of this evolution of successful designs. at the very bottom of the 2nd page? Relate this point to his overall argument. 4. Hoare compares programmers to craftsmen, high priests, and eventually engineers. How do you think he would compare them to scientists? 5. What is John Rushby advocating? 6. Reconcile the following statments made by Fred Brooks: The purpose of a programming system is to make a computer easy to use. (page 42) *Simplicity* is not enough. (page 44) the conceptual integrity of a system determines its ease of use. (page 46) discipline is good \[for\] art ... "Form is Liberating" (page 46-47) The discussion begun on page 254 may help you do so, or you may find it to be merely redundant of his claims without elucidating them. 7. Which of Beck's points do you find the most suprising? Are there additional parts of a good software engineering process that he seems to be missing? 8. Which of Rosenberg's arguments do you find the most compelling? Which is the least compelling? 9. Choose two opposing authors and relate their arguments. All of these authors are intelligent, educated people; take both sides of the argument seriously. ## Problem Set 2 [Problem Set 2](https://groups.csail.mit.edu/sdg/6.894/assignments/ps2.html) - Static Alloy Model *(due Wed March 9)* Now that you have developed some skills writing and analyzing models in Alloy, it's time to do something more interesting. This week's assignment is to construct a model of a subject of your own choosing. It should be a static model, meaning that there should be no modelling of mutable state. This doesn't mean that you can't specify operations that are executed dynamically (such as lookups), but there won't be an explicit notion of state. Your model should be presented as a self-contained case study. You should assume that your reader knows Alloy, but has no knowledge of the subject of the study. The writeup should include at least the following elements: - **(1)** an introduction explaining what's being studied, why it's interesting; - **(2)** an informal overview of the subject, outlining the key concepts; - **(3)** a detailed presentation of, and commentary on, the Alloy model; - **(4)** a conclusion, explaining what was learned, and evaluating to what extent modelling and analyzing the subject was helpful. Your model should include at least a couple of interesting simulations and at least one interesting assertion. You should concentrate on developing the model, and only polish the writeup after the model is largely complete. The model should be small and simple: your aim is to capture the essence of your subject as succinctly as possible. As a rough guide, you should expect to develop a model that has at least 3 signatures and 3 fields, but no more than about 8 signatures and 12 fields. Use Alloy to help you check refactorings of your constraints to reduce them to a concise, elegant (and understandable!) form. If your model has become complicated and arcane, try and identify aspects of it that aren't essential, or try to find a way to take a more abstract view that will preserve the core content while removing extraneous detail. As examples of case studies developed by students with comparable experience in Alloy, see: - [Chord: A Peer-to-Peer Protocol](https://groups.csail.mit.edu/sdg/6.894/assignments/chord.pdf) by Hoeteck Wee - [Case Study in Alloy Modeling: A Common Profile for Presence](https://groups.csail.mit.edu/sdg/6.894/assignments/instant-messaging.pdf) by Edmond Lau Both of these took several weeks of work, and involved extensive background reading. You should be less ambitious, and pick a subject that you already have some knowledge of, and can be confident you can model in a few hours. It's better to construct a simple model and polish it into something elegant and insightful than to construct a complicated model that you don't have time to rework. You can pick any subject that appeals to you. Here are some suggestions: - **DNS lookup:** model the structure of domain names, the contents of server databases, and the algorithm for resolving lookups; - **make file:** model the structure of a make file, and the calculation of which commands are to be executed given freshness data about files; - **style sheets:** model the structure of hierarchical style sheets, as found in programs such as Word, InDesign, Quark, and Framemaker, paying attention in particular to how inheritance of formatting properties is handled; - **web addressing:** model the way in which resources are named on the web, and the mechanisms used for resolving them; - **vote tallying:** model the relationship between a collection of ballots in which candidates are ranked, and the outcome of the election under different voting strategies (such as plurality, condorcet, borda count, instant runoff voting). ## Reading C [Reading C](https://groups.csail.mit.edu/sdg/6.894/assignments/readingC.html) - Z Specifications *(due Mon March 14)* 1. [J. M. Spivey](http://spivey.oriel.ox.ac.uk/mike/). *The Z Notation: A Reference Manual*. NY: [Prentice Hall](http://www.prenticehall.com/), 1988-2001. Website: [http://spivey.oriel.ox.ac.uk/~mike/zrm/](http://spivey.oriel.ox.ac.uk/~mike/zrm/) 2. [Carroll Morgan](http://www.cse.unsw.edu.au/~carrollm/). *Specification Case Studies: Telephone Network*. [Ian Hayes](http://www.itee.uq.edu.au/~ianh/sigpubs.html) (editor). [Prentice Hall](http://www.prenticehall.com/), 1987. 3. J. Michael Spivey. *Specifying a Real-Time Kernel*. IEEE, Sept. 1990. **Alternate to #3:** Roger Gimson and [Carroll Morgan](http://www.cse.unsw.edu.au/~carrollm/). *Specificiation Case Studies: The Role of Mathematics*. [Ian Hayes](http://www.itee.uq.edu.au/~ianh/sigpubs.html) (editor). [Prentice Hall](http://www.prenticehall.com/), 1987. 4. [Martin Fowler](http://www.martinfowler.com/). *Patterns for things that change with time*. [http://www.martinfowler.com/ap2/timeNarrative.html](http://www.martinfowler.com/ap2/timeNarrative.html) ### Study Questions C Be concise, clear, and thoughtful; a paragraph should suffice. Insight will be rewarded. 1. In John Spivey's Z Reference Manual, what is meant by the term 'view'? Give an example other than the one he uses. (The term is first used at the bottom of page 2, but you will need to read more of the article to understand what Spivey is getting at.) 2. In section 3.2.1 of Carroll Morgan's case study, how are implicit constraints being used in the definition of Call? That is, why does the given specification connect the caller to the recipient? 3. Discuss which parts of Spivey's analysis lend themselves to automation and which do not. **Alternate:** Roger Gimson is obviously a fan of mathematical specification. What is the key idea or guiding philosophy he is trying to get across with his case study? 4. What does Martin Fowler mean by "multiple dimensions of time"? Give an example other than the one he uses. ## Reading D [Reading D](https://groups.csail.mit.edu/sdg/6.894/assignments/readingD.html) - Beyond Interfaces 1. [Carl A. Gunter](http://www.cis.upenn.edu/~gunter/), [Elsa L. Gunter](http://www.cs.njit.edu/~elsa/), [Michael Jackson](http://mcs.open.ac.uk/mj665/), and [Pamela Zave](http://www.research.att.com/info/pamela). *A Reference Model for Requirements and Specifications*. [IEEE Software](http://www.computer.org/software/): Volume 17, Issue 3, May 2000, Pages: 37-43. 2. [David Lorge Parnas](http://www.cas.mcmaster.ca/sqrl/parnas.homepg.html). *Requirements Documentation: A Systematic Approach*. Slides from a talk given Feb 2003. **(Only read the first 30 slides.)** 3. [Michael Jackson](http://mcs.open.ac.uk/mj665/), "Specifications", from *Software Requirements And Specifications*, [Addison-Wesley Addison Wesley Professional](http://www.awprofessional.com/index.asp), 1995. 4. [Michael Jackson](http://mcs.open.ac.uk/mj665/), "Designations", from *Software Requirements And Specifications*, [Addison-Wesley Addison Wesley Professional](http://www.awprofessional.com/index.asp), 1995. 5. [Michael Jackson](http://mcs.open.ac.uk/mj665/), "Narrow Bridge", from *Software Requirements And Specifications*, [Addison-Wesley Addison Wesley Professional](http://www.awprofessional.com/index.asp), 1995. 6. *Safety Recommendations A-05-03 through -07*. [National Transportation Safety Board](http://www.ntsb.gov/). Washington, DC 20594. March 08, 2005. ### Study Questions D Be concise, clear, and thoughtful; a paragraph or two should suffice. Insight will be rewarded. Contention is encouraged. 1. How does Parnas's four variable model differ from the approach used by Gunter et. al.? 2. According to Gunter et. al., what is the difference between specifications and requirements? How would you classify the NTSB report? 3. Michael Jackson introduces the notion of a designation, which relates the world with an abstraction, and distinguishes it from a definition, which relates different parts of the abstraction. Give an example not derived from Lewis Carroll, and talk through it using his terminology. 4. Discuss some ideas from the readings that reflect the concerns given in the NTSB report. ## Problem Set 3 [PS3](https://groups.csail.mit.edu/sdg/6.894/assignments/ps3.html) - Dynamic Alloy Model This is the second of a pair of assignments using Alloy to model a system of your own choosing. Whereas in the first assignment, you considered only static aspects, in this assignment, you'll build a model with dynamic behaviour. If you want to, you can extend the static model from the previous assignment, but you'll be expected to show a real increment, and to write a new report. Your model should be presented as a self-contained case study. You should assume that your reader knows Alloy, but has no knowledge of the subject of the study. The writeup should include at least the following elements: - **(1)** an introduction explaining what's being studied, and why it's interesting; - **(2)** an informal overview of the subject, outlining the key concepts; - **(3)** a detailed presentation of, and commentary on, the Alloy model; - **(4)** a conclusion, explaining what was learned, and evaluating to what extent modelling and analyzing the subject was helpful. Your model should include at least a couple of interesting simulations and at least one interesting assertion. You should concentrate on developing the model, and only polish the writeup after the model is largely complete. The model should be small and simple: your aim is to capture the essence of your subject as succinctly as possible. As a rough guide, you should expect to develop a model that has at least 3 signatures and 3 fields, but no more than about 8 signatures and 12 fields. Use Alloy to help you check refactorings of your constraints to reduce them to a concise, elegant (and understandable!) form. If your model has become complicated and arcane, try and identify aspects of it that aren't essential, or try to find a way to take a more abstract view that will preserve the core content while removing extraneous detail. When appropriate, you should make use of the patterns taught in lecture, and cite them when you use them: abstract state machine, declarative operation, local state, implicit invariant, invariant preservation, trace, etc. A rough draft of the book chapters on these patterns is available on the private readings page. As examples of case studies developed by students with comparable experience in Alloy, see: - [Chord: A Peer-to-Peer Protocol](https://groups.csail.mit.edu/sdg/6.894/assignments/chord.pdf) by Hoeteck Wee - [Case Study in Alloy Modeling: A Common Profile for Presence](https://groups.csail.mit.edu/sdg/6.894/assignments/instant-messaging.pdf) by Edmond Lau Both of these took several weeks of work, and involved extensive background reading. You should be less ambitious, and pick a subject that you already have some knowledge of, and can be confident you can model in a few hours. It's better to construct a simple model and polish it into something elegant and insightful than to construct a complicated model that you don't have time to rework. You can pick any subject that appeals to you. Here are some suggestions: - **concurrency control:** verify a schemes involving mutexes, semaphores, locks, etc. Consider questions about deadlock, livelock, and starvation. For a starting point, see Ilya Shlyakhter's model examples/algorithms/dijkstra.als, included in the Alloy release; - **Unix file system:** model and analyze file system operations at the inode level; consider, for example, reclaiming unused blocks; - **caching strategies:** specify a detailed caching strategy and show that it conforms to a simple, abstract, non-deterministic description; - **cellular automata:** implement a cellular automaton framework in Alloy, and check theorems about it, or generate interesting cases. See Manu Sridharan's model examples/toys/life.als, included in the Alloy distribution. - **distributed algorithm:** find a small algorithm, such as a leader election algorithm, and verify it; - **elevator:** consider a bank of elevators with an arbitrary number of regular elevators and one or more freight elevators, serving an arbitrary number of floors, and characterize the desirable behaviours as a set of rules, as independent from one another as possible; \[warning: this is a very hard problem!\] - **style sheets:** model the behaviour of hierarchical style sheets, as found in programs such as Word, InDesign, Quark, and Framemaker, paying attention in particular to how inheritance of formatting properties is handled, and to what happens when styles are deleted - **buffer management:** model how applications typical handle multiple files, with buffers, recent file lists, etc; - **catalog views:** model an application (such as [iView Media Pro](http://www.iview-multimedia.com/)) in which assets (such as photos or email messages) can be classified in multiple ways, appearing in more than one folder at a time. ## Problem Set 4 [PS4](https://groups.csail.mit.edu/sdg/6.894/assignments/ps4.html) - Modal Logic and Model Checking with NuSMV The short essay entitled *Dekker* (available on the private course web site) describes a series of attempts, some flawed, to solve the mutual exclusion problem. Your task in this problem set is to model each of the 4 attempts, to write appropriate specifications in temporal logic, and to analyze them for counterexamples. You should use the NuSMV model checker, which you can download from the [NuSMV website](http://nusmv.irst.itc.it/NuSMV/download/getting-v2.html). Make sure you select the version that includes the Chaff SAT solver (so that you can do bounded analyses of LTL specifications). You will also need to download and install the Expat package, which can be downloaded from [sourceforge](http://sourceforge.net/projects/expat/). The Expat download comes with these [instructions](https://groups.csail.mit.edu/sdg/6.894/assignments/expat.txt) for installing it. You should install and run NuSMV right away so that we have time to help you if you encounter technical problems. Running NuSMV is easy. Execute bin/NuSMV and pass it a file containing an SMV machine. This will syntax-check the machine and check any CTL/LTL specs in that file. There is an exellent [tutorial](http://nusmv.irst.itc.it/NuSMV/tutorial/index.html) available from the website which will show you how to write and check NuSMV models. The [NuSMV website](http://nusmv.irst.itc.it/) also contains a number of examples, but most of them are quite complex; the examples in the tutorial are much more managable. You may find the following two examples written by the TA of some help: [trafficlight.smv](https://groups.csail.mit.edu/sdg/6.894/models/trafficlight.smv), [trafficlight2.smv](https://groups.csail.mit.edu/sdg/6.894/models/trafficlight2.smv). The NuSMV distribution contains the following model about semaphore which will help you to structure your models (but which solves a slightly different algorithm): [semaphore.smv](https://groups.csail.mit.edu/sdg/6.894/models/semaphore.smv). Your solution should include: - **\*** 4 models, corresponding to Versions 1 through 4 of the mutual exclusion algorithm in the essay; - **\*** For each model, a few appropriate temporal logic specifications that illustrate the points made in the text; - **\*** The results of checking each of the specifications; - **\*** A brief commentary explaining what you did and what you learned from it. What were the strengths and weaknesses of this style of modeling? You should make an effort to write specifications in both LTL and CTL, explaining why you choose one formalism over the other. ## Problem Set 5 [PS5](https://groups.csail.mit.edu/sdg/6.894/assignments/ps5.html) - Proving the Correctness of a Procedure This assignments comprises 3 parts: reading 4 classic papers with study questions, running ESC/Java on a simple program, and working out a simple proof using weakest preconditions. ### Reading These papers are available for download from the private website to which students of the course have access. 1. C. A. R. Hoare. *An Axiomatic Basis for Computer Programming*. Volume 12, Issue 10 (October 1969). Pages 576-580. ISSN 0001-0782 ACM Press. New York, NY, USA. 2. E.W. Dijkstra. *EWD472: Guarded commands, non-determinacy and formal derivation of programs*. Communications of the ACM 18 (1975), 8: 453-457. 3. Jon Bentley. *Programming Pearls*. Addison-Wesley, 1986. ISBN 0-201-10331-1 4. Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. *Extended Static Checking for Java*. Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation. Berlin, Germany, 2002. Pages 234-245. ACM Press. New York, NY, USA. ISBN: 1-58113-463-0. ### Study Questions 1. What now seems dated about Hoare's motivation for this paper? 2. Why is Euclid's Algorithm natural to write with guarded commands? Sketch out the algorithm in this style. What does it compute? 3. What does Bentley think about the roles of testing versus verification? 4. ESC/Java usually gives correct feedback, but it does not make any guarantees. Why is ESC/Java not sound? Why is it not complete? ### ESC/Java ESC/Java is easy to run. You can download pre-compiled versions from either [Compaq](http://research.compaq.com/SRC/esc/), its original developer, or from [Kind Software](http://www.kindsoftware.com/products/opensource/ESCJava2/), its current developers. The latter supports more platforms (such as Mac) and may be more up-to-date. Choose **one** of the following two Java programs and annotate it enough to get it through ESC/Java: [courses.java](https://groups.csail.mit.edu/sdg/6.894/assignments/courses.java) **or** [MyArrays.java](https://groups.csail.mit.edu/sdg/6.894/assignments/MyArrays.java). The first is an example developed by John Hatcliff and Matt Dwyer for use in a course on Software Specifications. The second is a pruned version of Java.util.Arrays. The second option is a more realistic example but will require slightly more annotations. There is ample [online documentation](http://www.kindsoftware.com/products/opensource/ESCJava2/ESCTools/docs/ESCJAVA-UsersManual.html) available, but here are a few pointers to get started. Annotations are written as comments and must begin with the tokens "//@" and end with a semicolon, ";". There are 5 types of annotations that you will be using: requires, ensures, assert, assume, invariant. Most of the annotations you write will be requires statements, which add preconditions to procedures. For example, you might write the following right before a method definition: ``` //@ requires x > 0 ==> y >= 0; ``` & means "and", | means "or", and \==> means "then". You can use quantification and type comparisons as follows (<: means subtype): ``` //@ requires \\forall int i; i < a.length ==> a\[i\] = null; //@ requires \\typeof (x) <: \\type (Object)); ``` Writing a precondition tells ESC to do 3 things: (a) make sure that the preconditions are sufficient to ensure any post-conditions will be satisfied, (b) make sure that the preconditions prevent out-of-bounds and null pointer exceptions, (c) make sure that all call sites obey the preconditions. You can add postconditions to a procedure by writing an ensures annotation just before the procedure definition. ``` //@ ensures \\result == a | \\result == 0; ``` ESC/Java is neither sound nor complete in general, so you may sometimes get false error reports. ESC is not able to do arbitrarily complex arithmetic -- for example it may not be able to infer that a value is non-negative if that value is produced via numerical computation. In such a case, you would need to add an assume clause: ``` //@ assume x > 0; ``` Clearly, you should use assume statements as little as possible. If you want to check other properties, you can write assert statements. For example, to claim that a pointer p is non-null, you would write the following: ``` //@ assert p != null; ``` Lastly, after a variable declaration, you can state an invariant on that variable. For example, ``` int x = 0; //@ invariant x >= 0; ``` ### Proof Exercise Consider the following procedure which puts a value into an array of key-value pairs at a specified key: ``` void put( Entry[] a, Key k, Val v) {     int i = 0;     while (i < a.length) {         if (a[i].key = k)             a[i].val = v         i = i+1;     } } ``` Assume there is a helper class Entry: ``` class Entry { Key key; Val val; } ``` Deduce the weakest precondition that guarantees the following postcondition: ``` all 0 <= i < a.length() . if (a_0[i].key_0 = k)           then (a[i].val = 0)           else (a[i].val = a_0[i].val_0) ``` key\_0, a\_0, and val\_0 are the values of key, a, and val in the pre-state. Show your proof as a proof outline -- i.e. code annotated/interwoven with assertions (in the style that we summarized Hoare proofs). Examples of weakest precondition proofs can be found in the scanned lecture notes. ### What to Hand In Your solution should include: - answers to the 4 study questions; - an annotated Java program that passes ESC/Java without any warnings, plus a short discussion of your experience using the tool; and - a proof outline for the weakest precondition exercise. ## Reading E [Reading E](https://groups.csail.mit.edu/sdg/6.894/assignments/readingE.html) - The Nature of Bugs in Software The topic for this last set of readings is code correctness and the nature of bugs. Your readings include a classic lecture by Dijkstra (EWD303) in which he argued the futility of testing, as well as some answers he gave to questions from a software engineering class at UT Austin. The paper by Martyn Thomas also comes from the formal methods culture -- Thomas was the founder of Praxis Critical Systems, a leading formal methods company -- but takes a perspective based more in engineering than mathematics. The paper by Michael Jackson illustrates the futility of incremental debugging in contrast not to verification, but to a programming method (called JSP) in which the program mirrors the structure of the data it processes. You'll see in it the structure diagram notation discussed in class this week. The 'Cathedral and the Bazaar' is a much-cited paper that makes the case for the open -source model, with an emphasis on incremental development and manual code review; it includes a discussion of the claim that 'all bugs are shallow'. PDFs of the readings can be downloaded from a private website to which students have access. Please recall the somewhat entrancing [submission instructions](https://groups.csail.mit.edu/sdg/6.894/submissions.html). 1. Eric Steven Raymond. *The Cathedral and the Bazaar*. O'Reilly Publishing. 1997-2001. ISBN: 0-596-00108-8. website: [http://www.catb.org/~esr/writings/cathedral-bazaar/cathedral-bazaar/](http://www.catb.org/~esr/writings/cathedral-bazaar/cathedral-bazaar/), [http://www.firstmonday.org/issues/issue3\_3/raymond/](http://www.firstmonday.org/issues/issue3_3/raymond/) 2. Martyn Thomas. *A View from the Stern*. Safety Critical Systems Club newsletter. The Centre for Software Reliability at Newcastle University. January, 2005. 3. [Michael Jackson](http://mcs.open.ac.uk/mj665/). "Getting it Wrong - A Cautionary Tale". [John R. Cameron](http://www.medphysics.wisc.edu/~jrc/), editor. *JSP and JSD: The Jackson Approach to Software Development*. Washington: [IEEE Computer Society Press](http://www.ieee.org/organizations/pubs/press/), 1989. ISBN:0-8186-8858-0 Website: [http://portal.acm.org/citation.cfm?id=77053&dl=ACM&coll=GUIDE](http://portal.acm.org/citation.cfm?id=77053&dl=ACM&coll=GUIDE) 4. E. W. Dijkstra. *On the Reliability of Programs (EWD 303)*. website: [http://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EWD303.html](http://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EWD303.html) 5. E. W. Dijkstra. *Student Questions*. website: [http://www.cs.utexas.edu/~almstrum/cs373/general/EWD/dijkstra-questions7-fa00.html](http://www.cs.utexas.edu/~almstrum/cs373/general/EWD/dijkstra-questions7-fa00.html) E. W. Dijkstra. *Answers to Student Questions: EWD 1305*. ### Study Questions E Be concise, clear, and thoughtful; a paragraph or two should suffice. Insight will be rewarded. Contention is encouraged. 1. What is meant by Raymond's claim that all bugs shallow? Do you think this is a good philosophy? 2. Contrast Thomas's view on testing with Raymond's view. 3. What is the moral of this story? 4. Do you believe the P^N back-of-the-envelope calculation of correctness? 5. Give your reactions to some of Dijkstra's controversial responses. ## Final Project [Final Project](https://groups.csail.mit.edu/sdg/6.894/assignments/fp.html) Your final project is an opportunity to explore ideas we've studied more deeply, to get some experience with a more realistic practical application, or to learn about an approach that we haven't covered but which fits within the purview of the course. ### Project Ideas Here are some ideas to help you get started thinking about possible projects. 1. Take a design or spec that's already described in some detail in a published paper and build a formal model and analyze it using Alloy or a model checker. For example, - N. Feamster, J. Winick, and J. Rexford. *A Model of BGP Routing for Network Engineering*. Proc. ACM SIGMETRICS, New York, NY, June 2004 [(pdf)](http://nms.lcs.mit.edu/~feamster/papers/emu-sigm2004.pdf) - *Bonjour Technical Specification*. Apple Computer [(pdf)](http://images.apple.com/macosx/pdf/MacOSX_Bonjour_TB.pdf) - S. Gavrila, J. Barkley. *Formal Specification for Role Based Access Control User/Role and Role/Role Relationship Management*. (1998), Third ACM Workshop on Role-Based Access Control. [(pdf)](http://csrc.nist.gov/rbac/gavrila-barkley-98.pdf). See other papers at [(website)](http://csrc.nist.gov/rbac/) 2. Construct a series of small models for some course material in computer or software systems, to make the material more precise, and to clarify and crystallize the key properties. For example, you could take one of the chapters of the 6033 text on memory hierarchy, naming or transactions: all should be fairly straightforward to express and analyze with Alloy or a model checker. The course notes for 6.826 (Principles of Computer Systems) include many interesting examples already expressed in SPEC, a formal language; you could translate some examples into a checkable language and do some analysis. [(website)](http://web.mit.edu/6.826/www/notes/) 3. Construct and analyze a metamodel to investigate some aspect of formal analysis. For example, you could model the abstraction function method with a state machine and a trace semantics, and show that if an abstraction function exists, you have trace inclusion. Or perhaps you could model the semantics of LTL and CTL, and show that certain formulas imply others. 4. Learn how to use a new tool, experiment with it on some small examples, and compare it to the tools you've seen. We recommend in particular: - The SPIN model checker, which accepts LTL specs and has a modelling language based on guarded commands, written in a C-like notation; [(website)](http://spinroot.com/spin/whatispin.html) - The LTSA verification tool, which is based on a process algebra called FSP; a very different formalism than the ones we studied, but a very nicely packaged tool with lots of good examples (and a book to go with it that I can lend you); [(website)](http://www.doc.ic.ac.uk/~jnm/book/ltsa/LTSA.html) - The Bogor model checker, which offers a high-level modelling language and a pluggable architecture [(website)](http://bogor.projects.cis.ksu.edu/) 5. Investigate a novel application of analysis technology. For example, it should be possible to use Alloy to check Hoare logic proof outlines. You could do this for an object-oriented program, by representing instance variables as relations.