-- typeConsistencyOfStore.tioga
-- Sturgis, March 21, 1989 10:59:02 am PST
-- Spreitze, May 9, 1991 1:57 pm PDT
[This is Howard's typeConsistencyOfStore.tioga of 21-Mar-89 10:59:02 PST, with the missing parenthesis in the legality requirement for Store added, one of the two D's renamed to , and formatting changes. See my typeConsistencyOfStoreValues.tioga for a justification of Howard's legality requirement for Store. MJS, May 9, 1991]
We take a very simple model.
There is a set of variables, V. There is a configuration, G: V b U, where U is the set of values. V † U.
We have one operation: Store from
v
1 through
v
2, for
v
1 and
v
2 in
V. This is successful only if
G(
v
2)
V. When it is successful, it produces a new configuration
G
`, where
G
` is defined by:
if v ` G(v2) then G`(v) = G(v).
if v = G(v2) then G`(v) = G(v1).
We have a set of types, T. We have a typing, an assignment of types to the variables, : V b T. For the moment, we assume that the typing is fixed.
The types really belong to an algebra. This algebra has (for the moment) two unary operations: load and store. That is, for some types t in T, t.load and t.store are defined and also in T.
Given a typing,
, and a type,
t, we have a set of values:
D(
t)
†
U. We make only one assumption (for the moment) about this set of values:
for
v
V, if
v
D(
t), then
D((v)) † D(t.load), and
D(t.store) † D((v)).
We say that a configuration
G is consistent with a typing
if and only if
for all v in V, G(v) D((v)).
Now, we restrict Store to also require:
Store from
v
1 through
v
2 is legal for typing
only if
D((v1)) † D((v2).store)
Now, we attempt to prove that: if G is consistent with a typing , Store from v1 through v2 is legal for typing , and Store from v1 through v2 succeeds for G, producing G`, then G` is consistent with .
We must prove that
G
`(
v)
D(
(
v)), for all
v in
V. Let
v
3 =
G(
v
2).
if v ` v3, then G`(v) = G(v), and the conclusion follows from the assumption that G is consistent with .
So, to complete the proof, we need only prove that G`(v3) D((v3)).
G
`(
v
3) =
G(
v
1)
by definition of v3 and the definition of G`.
G(
v
1)
D(
(
v
1))
by the assumption that G is consistent with D.
D(
(
v
1))
†
D(
(
v
2).store)
by the assumption that a store from v1 through v2 is legal for .
D(
(
v
2).store)
†
D(
(
v
3))
This requires several steps.
G(
v
2)
D(
(
v
2))
because G is consistent with D
v
3
D(
(
v
2))
because v3 = G(v2)
letting
t =
(
v
2), we have
v3 D(t)
hence
D(
t.store)
†
D(
(
v
3))
by our assumption about lt.D(t)
D(
(
v
2).store)
†
D(
(
v
3))
from D(t.store) † D((v3)) and t = (v2)
Collecting, we have
G`(v3) D((v3)), as desired.