Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav07_homework_2 [2007/03/29 22:21] vkuncak |
sav07_homework_2 [2007/04/06 20:15] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Homework 2 ====== | ====== Homework 2 ====== | ||
| + | |||
| Line 10: | Line 11: | ||
| F ::= A | (F&F) | (F|F) | ~F | ALL v.F | EX v.F | F ::= A | (F&F) | (F|F) | ~F | ALL v.F | EX v.F | ||
| - | A ::= v=v | v + K <= v | + | A ::= v=v | v + K ≤ v |
| K ::= ... -2 | -1 | 0 | 1 | 2 | ... | K ::= ... -2 | -1 | 0 | 1 | 2 | ... | ||
| v ::= x | y | z | ... | v ::= x | y | z | ... | ||
| Line 30: | Line 31: | ||
| 1. Implement a verification condition generator that takes abstract syntax trees of the following form | 1. Implement a verification condition generator that takes abstract syntax trees of the following form | ||
| - | S ::= (x=T) | + | S ::= (v=T) |
| | assume(F) | | assume(F) | ||
| | assert(F) | | assert(F) | ||
| Line 37: | Line 38: | ||
| | while [inv F] (F) { S } | | while [inv F] (F) { S } | ||
| | if (F) { S } else { S } | | if (F) { S } else { S } | ||
| - | T ::= T+T | T-T | K*T | v | + | T ::= T+T | T-T | K*T | v | K |
| - | A ::= T=T | T < T | + | A ::= T=T | T < T | True | False |
| F ::= A | (F&F) | (F|F) | ~F | ALL v.F | EX v.F | F ::= A | (F&F) | (F|F) | ~F | ALL v.F | EX v.F | ||
| K ::= 0 | 1 | 2 | ... | K ::= 0 | 1 | 2 | ... | ||