Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:proving_correctness_of_some_small_examples [2008/02/17 18:38] vkuncak |
sav08:proving_correctness_of_some_small_examples [2008/02/17 18:56] vkuncak |
||
|---|---|---|---|
| Line 7: | Line 7: | ||
| Consider the following recursive function: | Consider the following recursive function: | ||
| - | <code java> | + | <code> |
| private static int f(int x, int y) | private static int f(int x, int y) | ||
| { | { | ||
| Line 22: | Line 22: | ||
| } | } | ||
| </code> | </code> | ||
| + | |||
| + | * What does 'f' compute? | ||
| + | * How can we prove it? | ||
| + | * [[Proof of first lecture01 example]] | ||
| {{sav08:integerdemo.java.txt|Examples of Functions with Specifications}} | {{sav08:integerdemo.java.txt|Examples of Functions with Specifications}} | ||