equal
deleted
inserted
replaced
6 |
6 |
7 theory Memory |
7 theory Memory |
8 imports MemoryParameters ProcedureInterface |
8 imports MemoryParameters ProcedureInterface |
9 begin |
9 begin |
10 |
10 |
11 types |
11 type_synonym memChType = "(memOp, Vals) channel" |
12 memChType = "(memOp, Vals) channel" |
12 type_synonym memType = "(Locs => Vals) stfun" (* intention: MemLocs => MemVals *) |
13 memType = "(Locs => Vals) stfun" (* intention: MemLocs => MemVals *) |
13 type_synonym resType = "(PrIds => Vals) stfun" |
14 resType = "(PrIds => Vals) stfun" |
|
15 |
14 |
16 consts |
15 consts |
17 (* state predicates *) |
16 (* state predicates *) |
18 MInit :: "memType => Locs => stpred" |
17 MInit :: "memType => Locs => stpred" |
19 PInit :: "resType => PrIds => stpred" |
18 PInit :: "resType => PrIds => stpred" |