blob: 239bd6b71039a9c4f3d1b918b6747056c89730b0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
Require Export Language.
Module Type Conversion (A B: Language).
Parameter convertProgram: forall (x: A.Params) (y: B.Params),
A.Program x -> option (B.Program y).
Parameter convertState: forall (x: A.Params) (y: B.Params),
B.State y -> option (A.State x).
Axiom convert_spec: forall pa pb a a' b b' prog prog',
convertProgram pa pb prog = Some prog' ->
convertState pa pb a = Some a' ->
convertState pa pb b = Some b' ->
B.evaluatesTo pb prog' a b <-> A.evaluatesTo pa prog a' b'.
End Conversion.
|
