equal
deleted
inserted
replaced
6 - variables are typed. |
6 - variables are typed. |
7 - the state space is uniform, common to all defined programs. |
7 - the state space is uniform, common to all defined programs. |
8 - variables can be quantified over. |
8 - variables can be quantified over. |
9 *) |
9 *) |
10 |
10 |
11 header{*UNITY Program States*} |
11 section{*UNITY Program States*} |
12 |
12 |
13 theory State imports Main begin |
13 theory State imports Main begin |
14 |
14 |
15 consts var :: i |
15 consts var :: i |
16 datatype var = Var("i \<in> list(nat)") |
16 datatype var = Var("i \<in> list(nat)") |