equal
deleted
inserted
replaced
31 <DD> the letters a-z are interpreted as program variables, |
31 <DD> the letters a-z are interpreted as program variables, |
32 all other identifiers as mathematical variables.<P> |
32 all other identifiers as mathematical variables.<P> |
33 </DL> |
33 </DL> |
34 The pre/post conditions can be arbitrary HOL formulae including program |
34 The pre/post conditions can be arbitrary HOL formulae including program |
35 variables. The program text should only refer to program variables. |
35 variables. The program text should only refer to program variables. |
|
36 <P> |
|
37 <B>Note</B>: Program variables are typed in the same way as HOL |
|
38 variables. Although you can write programs over arbitrary types, all |
|
39 program variables in a particular program must be of the same type! |
36 </BODY></HTML> |
40 </BODY></HTML> |