|
3807
|
1 |
(*
|
|
|
2 |
File: MemoryParameters.thy
|
|
|
3 |
Author: Stephan Merz
|
|
|
4 |
Copyright: 1997 University of Munich
|
|
|
5 |
|
|
|
6 |
Theory Name: MemoryParameters
|
|
|
7 |
Logic Image: TLA
|
|
|
8 |
|
|
|
9 |
RPC-Memory example: Memory parameters
|
|
|
10 |
*)
|
|
|
11 |
|
|
5184
|
12 |
MemoryParameters = Datatype + RPCMemoryParams +
|
|
3807
|
13 |
|
|
6255
|
14 |
(* the memory operations *)
|
|
|
15 |
datatype memOp = read Locs | write Locs Vals
|
|
|
16 |
|
|
3807
|
17 |
consts
|
|
|
18 |
(* memory locations and contents *)
|
|
6255
|
19 |
MemLoc :: Locs set
|
|
|
20 |
MemVal :: Vals set
|
|
3807
|
21 |
|
|
|
22 |
(* some particular values *)
|
|
|
23 |
OK :: "Vals"
|
|
|
24 |
BadArg :: "Vals"
|
|
|
25 |
MemFailure :: "Vals"
|
|
|
26 |
NotAResult :: "Vals" (* defined here for simplicity *)
|
|
|
27 |
|
|
|
28 |
(* the initial value stored in each memory cell *)
|
|
|
29 |
InitVal :: "Vals"
|
|
|
30 |
|
|
|
31 |
rules
|
|
|
32 |
(* basic assumptions about the above constants and predicates *)
|
|
6255
|
33 |
BadArgNoMemVal "BadArg ~: MemVal"
|
|
|
34 |
MemFailNoMemVal "MemFailure ~: MemVal"
|
|
|
35 |
InitValMemVal "InitVal : MemVal"
|
|
|
36 |
NotAResultNotVal "NotAResult ~: MemVal"
|
|
3807
|
37 |
NotAResultNotOK "NotAResult ~= OK"
|
|
|
38 |
NotAResultNotBA "NotAResult ~= BadArg"
|
|
|
39 |
NotAResultNotMF "NotAResult ~= MemFailure"
|
|
|
40 |
end
|