-- 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 D, 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 _ U, where U is the set of values.  V I U.We have one operation: Store from v1 through v2, for v1 and v2 in V.  This is successful only if G(v2) B 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, D: V _ 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, D, and a type, t, we have a set of values: D(t) I U.  We make only one assumption (for the moment) about this set of values:for v B V, if v B D(t), thenD(D(v)) I D(t.load), andD(t.store) I D(D(v)).We say that a configuration G is consistent with a typing D if and only iffor all v in V, G(v) B D(D(v)).Now, we restrict Store to also require:Store from v1 through v2 is legal for typing D only ifD(D(v1)) I D(D(v2).store)Now, we attempt to prove that: if G is consistent with a typing D, Store from v1 through v2 is legal for typing D, and Store from v1 through v2 succeeds for G, producing G(, then G( is consistent with D.We must prove that G((v) B D(D(v)), for all v in V.  Let v3 = G(v2).if v = v3, then G((v) = G(v), and the conclusion follows from the assumption that G is consistent with D.So, to complete the proof, we need only prove that G((v3) B D(D(v3)).G((v3) = G(v1)by definition of v3 and the definition of G(.G(v1) B D(D(v1))by the assumption that G is consistent with D.D(D(v1)) I D(D(v2).store)by the assumption that a store from v1 through v2 is legal for D.D(D(v2).store) I D(D(v3))This requires several steps.G(v2) B D(D(v2))because G is consistent with Dv3 B D(D(v2))because v3 = G(v2)letting t = D(v2), we havev3 B D(t)hence D(t.store) I D(D(v3))by our assumption about lt.D(t)D(D(v2).store) I D(D(v3))from D(t.store) I D(D(v3)) and t = D(v2)Collecting, we haveG((v3) B D(D(v3)), as desired.      Э╩)  Ш JШJШ*JШ$JШ IblockЪЬг╧gЬ╧mЬЧШ╩KЪЬШKЪЬ╧iЬЭЬЯЬЮЬЯЬЯЬЯЬЮЬЯЬШjЪЬ"Я╧dЬ	ЯаЬЯаЬЯаЬЯЬЭЬЯаЬЮЬЯЬ:ЭЮЬЭЮЬШ└IindentЪЬЯЬЮЬЭЬЯаЬЭЮЬЯЬЭЬЯЬШLЪЬЯЬЭЬЯаЬЭЮЬЯЬЭЬЯаЬШ ЧKШ KЪЬЯЬ>ЮЬЯЬЮЬЯЬ6ШХKЪЬЙЯЬЯЬЯЬ
ЯЬЯЬШ╛ЪЬЮЬЯЬЭЬЯЬЮЬЯЬIШМЪЬЯЬЮЬЯЬЯЬЮЬЭЬЯЬШLЪЭЬЮЬЯЬЮЬЭЬЯЬШLЪЭЬЯЬЮЬЭЬЮЬЯЬШЧЧЪЬЭЬЮЬШJLЪЬЯЬЯЬЭЬЯЬЮЬЭЬЮЬЯЬШЧШ'Ъ	ЬЯаЬ	ЯаЬЮЬШ6LЪЭЬЮЬЯаЬЮЬЭЬЮЬЯаЬШЧЧKШ KЪЬ"ЭЬЮЬЯаЬ	ЯаЬЮЬЯаЬ	ЯаЬЭЬЭЮЬЭЮЬЮЬШ╦KШ ЪЬЭЮЬЯЬЮЬЭЬЮЬЯЬЯЬЯЬЯаЬЭЬЯаЬШDLЪЬЯЬЮЬЯаЬЭЮЬЯЬЭЬЯЬ7ЭЬЮЬШiLЪЬ3ЭЮЬЯаЬЮЬЭЬЮЬЯаЬШEЪЭЮЬЯаЬЭЬЯаЬШLЪЬЯаЬЭЮЬШ-ЧЪЭЬЯаЬЮЬЭЬЮЬЯаЬШLЪЬЭЬЭЬШ.ЧЪЭЬЮЬЯаЬЮЬЭЬЮЬЯаЬШLЪ	Ь$ЯаЬ	ЯаЬЮЬШAЧЪЭЬЮЬЯаЬ	ЮЬЭЬЮЬЯаЬШШЪЭЬЯаЬЮЬЭЬЮЬЯаЬШLЪЬЭЬЭШЧЪЯаЬЮЬЭЬЮЬЯаЬШLЪ	ЬЯаЬЭЬЯаЬШЧЪЬЯЬЮЬЯаЬ
ШLЪ	ЯаЬЮЬЭЬЯЬШ	ЪЬЭЬЯЬЮЬЭЬЮЬЯаЬШLЪЬЭЯЬЭЬЯЬШЧЧЪЭЬЮЬЯаЬ	ЮЬЭЬЮЬЯаЬШLЪЬЭЬЯЬЮЬЭЬЮЬЯаЬЯЬЮЬЯаЬШ(ЧЧЧLШ ШLЪЭЮЬЯаЬЮЬЭЬЮЬЯаЬШЧLШ ЧЧ ЕЧ    
X  З  