|
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 |
|
|
|
12 |
MemoryParameters = Prod + Sum + Arith + RPCMemoryParams +
|
|
|
13 |
|
|
|
14 |
(* the memory operations. nb: data types must be defined in theories
|
|
|
15 |
that do not include Intensional -- otherwise the induction rule
|
|
|
16 |
can't be type-checked unambiguously.
|
|
|
17 |
*)
|
|
|
18 |
datatype Rd = read
|
|
|
19 |
datatype Wr = write
|
|
|
20 |
|
|
|
21 |
types
|
|
|
22 |
(* legal arguments for the memory *)
|
|
|
23 |
memArgType = "(Rd * Locs) + (Wr * Locs * Vals)"
|
|
|
24 |
|
|
|
25 |
consts
|
|
|
26 |
(* memory locations and contents *)
|
|
|
27 |
MemLoc :: "Locs => bool"
|
|
|
28 |
MemVal :: "Vals => bool"
|
|
|
29 |
|
|
|
30 |
(* some particular values *)
|
|
|
31 |
OK :: "Vals"
|
|
|
32 |
BadArg :: "Vals"
|
|
|
33 |
MemFailure :: "Vals"
|
|
|
34 |
NotAResult :: "Vals" (* defined here for simplicity *)
|
|
|
35 |
|
|
|
36 |
(* the initial value stored in each memory cell *)
|
|
|
37 |
InitVal :: "Vals"
|
|
|
38 |
|
|
|
39 |
rules
|
|
|
40 |
(* basic assumptions about the above constants and predicates *)
|
|
|
41 |
BadArgNoMemVal "~MemVal(BadArg)"
|
|
|
42 |
MemFailNoMemVal "~MemVal(MemFailure)"
|
|
|
43 |
InitValMemVal "MemVal(InitVal)"
|
|
|
44 |
NotAResultNotVal "~MemVal(NotAResult)"
|
|
|
45 |
NotAResultNotOK "NotAResult ~= OK"
|
|
|
46 |
NotAResultNotBA "NotAResult ~= BadArg"
|
|
|
47 |
NotAResultNotMF "NotAResult ~= MemFailure"
|
|
|
48 |
end
|
|
|
49 |
|
|
|
50 |
|