The Note Context in the rightmost column is only shown in case an annotated program exists. - You can navigate to the annotated program via the annotated slide view (= 'the note context').
| An algebraic specification of a stack. | stack.gas | Slide context | Text book context | - |
| An axiomatic specification of the squareroot function. | sqrt-specification | Slide context | Text book context | - |
| Circular list with preconditions and postconditions. | CircularListPrePost.java | Slide context | Text book context | - |
| Excerpt of highly responsible class Client of BankAccount. | bank-account.cs | Slide context | Text book context | - |
| Circular list with a class invariant. | CircularListInvariant.java | Slide context | Text book context | - |
| An abstract class with preconditions and postconditions. | stack.cs | Slide context | Text book context | - |
| Division by repeated subtraction. | div.cs | Slide context | - | - |
| Output of the division program. | div-output | Slide context | - | - |
| Division by repeated subtraction - instrumented with output inside loop. | instrumented-div.cs | Slide context | - | - |
| Output of the instrumented division program. | instrumented-div-output | Slide context | - | - |
Generated: Monday February 7, 2011, 12:22:06