:: Memory handling for SCM+FSA :: by Piotr Rudnicki and Andrzej Trybulec :: :: Received July 18, 1996 :: Copyright (c) 1996-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies SCMFSA_2, XBOOLE_0, AMI_1, GRAPHSP, AMI_3, FINSEQ_1, FUNCT_1, SUBSET_1, FINSUB_1, SETWISEO, CARD_1, TARSKI, RELAT_1, FINSET_1, NUMBERS, FUNCT_4, VALUED_1, ARYTM_3, AMISTD_2, XXREAL_0, SCMFSA6A, FSM_1, CIRCUIT2, STRUCT_0, ARYTM_1, INT_1, COMPLEX1, PARTFUN1, FINSEQ_2, NAT_1, SF_MASTR, RELOC, COMPOS_1, EXTPRO_1, SCMPDS_4, TURING_1, AMISTD_1, FUNCOP_1; notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, FINSET_1, FINSUB_1, NAT_1, INT_1, NAT_D, VALUED_1, STRUCT_0, SETWISEO, SEQ_4, CARD_3, FINSEQ_1, FINSEQ_2, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, FUNCT_4, PBOOLE, FUNCT_7, MEMSTR_0, COMPOS_0, COMPOS_1, COMPOS_2, AMI_2, EXTPRO_1, AMI_3, SCMFSA_2, AMISTD_2, SCMFSA6A, INT_2, XXREAL_0, SCMFSA_M; constructors SETWISEO, INT_2, SEQ_4, AMI_3, SCMFSA6A, RELSET_1, VALUED_1, AMISTD_2, AMISTD_1, AMI_2, SCMFSA_1, CARD_5, PRE_POLY, DOMAIN_1, PBOOLE, FUNCT_7, MEMSTR_0, SCMFSA_M, COMPOS_1, NAT_D, COMPOS_2; registrations FUNCT_1, ORDINAL1, RELSET_1, FINSET_1, FINSUB_1, XREAL_0, INT_1, SCMFSA_2, XBOOLE_0, VALUED_1, FINSEQ_1, AMISTD_2, SCMFSA10, COMPOS_1, EXTPRO_1, CARD_1, COMPOS_0, SCM_INST, NAT_1, SCMFSA6A, FUNCOP_1; requirements NUMERALS, BOOLE, SUBSET, REAL; begin :: Uniqueness of instruction components reserve a, b, c, a1, a2, b1, b2 for Int-Location, l, l1, l2 for Nat, f, g, f1, f2 for FinSeq-Location, i, j for Instruction of SCM+FSA, X, Y for set; theorem :: SF_MASTR:1 a1:=b1 = a2:=b2 implies a1 = a2 & b1 = b2; theorem :: SF_MASTR:2 AddTo(a1,b1) = AddTo(a2,b2) implies a1 = a2 & b1 = b2; theorem :: SF_MASTR:3 SubFrom(a1,b1) = SubFrom(a2,b2) implies a1 = a2 & b1 = b2; theorem :: SF_MASTR:4 MultBy(a1,b1) = MultBy(a2,b2) implies a1 = a2 & b1 = b2; theorem :: SF_MASTR:5 Divide(a1,b1) = Divide(a2,b2) implies a1 = a2 & b1 = b2; theorem :: SF_MASTR:6 goto l1 = goto l2 implies l1 = l2; theorem :: SF_MASTR:7 a1=0_goto l1 = a2=0_goto l2 implies a1 = a2 & l1 = l2; theorem :: SF_MASTR:8 a1>0_goto l1 = a2>0_goto l2 implies a1 = a2 & l1 = l2; theorem :: SF_MASTR:9 b1:=(f1, a1) = b2:=(f2, a2) implies a1 = a2 & b1 = b2 & f1 = f2; theorem :: SF_MASTR:10 (f1, a1):=b1 = (f2, a2):=b2 implies a1 = a2 & b1 = b2 & f1 = f2; theorem :: SF_MASTR:11 a1:=len f1 = a2:=len f2 implies a1 = a2 & f1 = f2; theorem :: SF_MASTR:12 f1:=<0,...,0>a1 = f2:=<0,...,0>a2 implies a1 = a2 & f1 = f2; begin :: Integer locations used in a macro instruction definition let i be Instruction of SCM+FSA; func UsedIntLoc i -> Element of Fin Int-Locations means :: SF_MASTR:def 1 ex a, b being Int-Location st (i = (a := b) or i = AddTo(a, b) or i = SubFrom(a, b) or i = MultBy(a, b) or i = Divide(a, b)) & it = {a, b} if InsCode i in {1, 2, 3, 4, 5} , ex a being Int-Location, l being Nat st (i = a =0_goto l or i = a>0_goto l) & it = {a} if InsCode i = 7 or InsCode i = 8, ex a , b being Int-Location, f being FinSeq-Location st (i = b := (f, a) or i = (f, a) := b) & it = {a, b} if InsCode i = 9 or InsCode i = 10, ex a being Int-Location, f being FinSeq-Location st (i = a :=len f or i = f :=<0,...,0>a) & it = {a} if InsCode i = 11 or InsCode i = 12 otherwise it = {}; end; theorem :: SF_MASTR:13 UsedIntLoc halt SCM+FSA = {}; theorem :: SF_MASTR:14 i = a:=b or i = AddTo(a, b) or i = SubFrom(a, b) or i = MultBy(a , b) or i = Divide(a, b) implies UsedIntLoc i = {a, b}; theorem :: SF_MASTR:15 UsedIntLoc goto l = {}; theorem :: SF_MASTR:16 i = a=0_goto l or i = a>0_goto l implies UsedIntLoc i = {a}; theorem :: SF_MASTR:17 i = b := (f, a) or i = (f, a) := b implies UsedIntLoc i = {a, b}; theorem :: SF_MASTR:18 i = a :=len f or i = f :=<0,...,0>a implies UsedIntLoc i = {a}; definition let X be set; func UsedILoc X -> Subset of Int-Locations equals :: SF_MASTR:def 2 union { UsedIntLoc i : i in X }; end; registration let X be finite set; cluster UsedILoc X -> finite; end; definition let p be Function; func UsedILoc p -> Subset of Int-Locations equals :: SF_MASTR:def 3 UsedILoc rng p; :: ex UIL being :: Function of the InstructionsF of SCM+FSA, Fin Int-Locations st (for i being :: Instruction of SCM+FSA holds UIL.i = UsedIntLoc i) & it = Union (UIL * p); end; registration let p be preProgram of SCM+FSA; cluster UsedILoc p -> finite; end; reserve p, r for preProgram of SCM+FSA, I, J for Program of SCM+FSA, k, m, n for Nat; theorem :: SF_MASTR:19 i in rng p implies UsedIntLoc i c= UsedILoc p; theorem :: SF_MASTR:20 UsedILoc(p +* r) c= UsedILoc p \/ UsedILoc r; theorem :: SF_MASTR:21 dom p misses dom r implies UsedILoc(p +* r) = UsedILoc p \/ UsedILoc r; theorem :: SF_MASTR:22 UsedILoc p = UsedILoc Shift(p, k); theorem :: SF_MASTR:23 UsedIntLoc i = UsedIntLoc IncAddr(i, k); theorem :: SF_MASTR:24 UsedILoc p = UsedILoc IncAddr(p, k); theorem :: SF_MASTR:25 UsedILoc I = UsedILoc Reloc(I, k); theorem :: SF_MASTR:26 UsedILoc I = UsedILoc Directed I; theorem :: SF_MASTR:27 UsedILoc (I ";" J) = (UsedILoc I) \/ (UsedILoc J); theorem :: SF_MASTR:28 UsedILoc Macro i = UsedIntLoc i; theorem :: SF_MASTR:29 UsedILoc (i ";" J) = (UsedIntLoc i) \/ UsedILoc J; theorem :: SF_MASTR:30 UsedILoc (I ";" j) = (UsedILoc I) \/ UsedIntLoc j; theorem :: SF_MASTR:31 UsedILoc (i ";" j) = (UsedIntLoc i) \/ UsedIntLoc j; begin :: Finite sequence locations used in macro instructions definition let i be Instruction of SCM+FSA; func UsedInt*Loc i -> Element of Fin FinSeq-Locations means :: SF_MASTR:def 4 ex a, b being Int-Location, f being FinSeq-Location st (i = b := (f, a) or i = (f, a) := b) & it = {f} if InsCode i = 9 or InsCode i = 10, ex a being Int-Location, f being FinSeq-Location st (i = a :=len f or i = f :=<0,...,0>a) & it = {f} if InsCode i = 11 or InsCode i = 12 otherwise it = {}; end; theorem :: SF_MASTR:32 i = halt SCM+FSA or i = a:=b or i = AddTo(a, b) or i = SubFrom(a , b) or i = MultBy(a, b) or i = Divide(a, b) or i = goto l or i = a=0_goto l or i = a>0_goto l implies UsedInt*Loc i = {}; theorem :: SF_MASTR:33 i = b := (f, a) or i = (f, a) := b implies UsedInt*Loc i = {f}; theorem :: SF_MASTR:34 i = a :=len f or i = f :=<0,...,0>a implies UsedInt*Loc i = {f}; definition let X be set; func UsedI*Loc X -> Subset of FinSeq-Locations equals :: SF_MASTR:def 5 union { UsedInt*Loc i : i in X }; end; definition let p be Function; func UsedI*Loc p -> Subset of FinSeq-Locations equals :: SF_MASTR:def 6 UsedI*Loc rng p; end; registration let X be finite set; cluster UsedI*Loc X -> finite; end; registration let p be preProgram of SCM+FSA; cluster UsedI*Loc p -> finite; end; theorem :: SF_MASTR:35 i in rng p implies UsedInt*Loc i c= UsedI*Loc p; theorem :: SF_MASTR:36 UsedI*Loc (p +* r) c= UsedI*Loc p \/ UsedI*Loc r; theorem :: SF_MASTR:37 dom p misses dom r implies UsedI*Loc (p +* r) = (UsedI*Loc p ) \/ (UsedI*Loc r); theorem :: SF_MASTR:38 UsedI*Loc p = UsedI*Loc Shift(p, k); theorem :: SF_MASTR:39 UsedInt*Loc i = UsedInt*Loc IncAddr(i, k); theorem :: SF_MASTR:40 UsedI*Loc p = UsedI*Loc IncAddr(p, k); theorem :: SF_MASTR:41 UsedI*Loc I = UsedI*Loc Reloc(I, k); theorem :: SF_MASTR:42 UsedI*Loc I = UsedI*Loc Directed I; theorem :: SF_MASTR:43 UsedI*Loc (I ";" J) = UsedI*Loc I \/ UsedI*Loc J; theorem :: SF_MASTR:44 UsedI*Loc Macro i = UsedInt*Loc i; theorem :: SF_MASTR:45 UsedI*Loc (i ";" J) = (UsedInt*Loc i) \/ UsedI*Loc J; theorem :: SF_MASTR:46 UsedI*Loc (I ";" j) = (UsedI*Loc I) \/ UsedInt*Loc j; theorem :: SF_MASTR:47 UsedI*Loc (i ";" j) = (UsedInt*Loc i) \/ UsedInt*Loc j; begin :: Choosing integer location not used in a macro instruction reserve L for finite Subset of Int-Locations; ::$CD theorem :: SF_MASTR:48 not FirstNotIn L in L; theorem :: SF_MASTR:49 FirstNotIn L = intloc m & not intloc n in L implies m <= n; definition let p be preProgram of SCM+FSA; func FirstNotUsed p -> Int-Location means :: SF_MASTR:def 8 ex sil being finite Subset of Int-Locations st sil = UsedILoc p \/ {intloc 0} & it = FirstNotIn sil; end; registration let p be preProgram of SCM+FSA; cluster FirstNotUsed p -> read-write; end; theorem :: SF_MASTR:50 not FirstNotUsed p in UsedILoc p; theorem :: SF_MASTR:51 a:=b in rng p or AddTo(a, b) in rng p or SubFrom(a, b) in rng p or MultBy(a, b) in rng p or Divide(a, b) in rng p implies FirstNotUsed p <> a & FirstNotUsed p <> b; theorem :: SF_MASTR:52 a=0_goto l in rng p or a>0_goto l in rng p implies FirstNotUsed p <> a; theorem :: SF_MASTR:53 b := (f, a) in rng p or (f, a) := b in rng p implies FirstNotUsed p <> a & FirstNotUsed p <> b; theorem :: SF_MASTR:54 a :=len f in rng p or f :=<0,...,0>a in rng p implies FirstNotUsed p <> a; begin :: Choosing finite sequence location not used in a macro instruction reserve L for finite Subset of FinSeq-Locations; definition ::$CD end; theorem :: SF_MASTR:55 not First*NotIn L in L; theorem :: SF_MASTR:56 First*NotIn L = fsloc m & not fsloc n in L implies m <= n; definition let p be preProgram of SCM+FSA; func First*NotUsed p -> FinSeq-Location means :: SF_MASTR:def 10 ex sil being finite Subset of FinSeq-Locations st sil = UsedI*Loc p & it = First*NotIn sil; end; theorem :: SF_MASTR:57 not First*NotUsed p in UsedI*Loc p; theorem :: SF_MASTR:58 b := (f, a) in rng p or (f, a) := b in rng p implies First*NotUsed p <> f; theorem :: SF_MASTR:59 a :=len f in rng p or f :=<0,...,0>a in rng p implies First*NotUsed p <> f; begin :: Semantics reserve s, t for State of SCM+FSA; reserve P for Instruction-Sequence of SCM+FSA; theorem :: SF_MASTR:60 not c in UsedIntLoc i implies Exec(i, s).c = s.c; theorem :: SF_MASTR:61 I c= P & (for m st m < n holds IC Comput(P,s,m) in dom I) & not a in UsedILoc I implies Comput(P,s,n).a = s.a; theorem :: SF_MASTR:62 not f in UsedInt*Loc i implies Exec(i, s).f = s.f; theorem :: SF_MASTR:63 I c= P & (for m st m < n holds IC Comput(P,s,m) in dom I) & not f in UsedI*Loc I implies Comput(P,s,n).f = s.f; theorem :: SF_MASTR:64 s | UsedIntLoc i = t | UsedIntLoc i & s | UsedInt*Loc i = t | UsedInt*Loc i & IC s = IC t implies IC Exec(i, s) = IC Exec(i, t) & Exec(i, s) | UsedIntLoc i = Exec(i, t) | UsedIntLoc i & Exec(i, s) | UsedInt*Loc i = Exec( i, t) | UsedInt*Loc i; theorem :: SF_MASTR:65 for P,Q being Instruction-Sequence of SCM+FSA st I c= P & I c= Q & Start-At(0,SCM+FSA) c= s & Start-At(0,SCM+FSA) c= t & s | UsedILoc I = t | UsedILoc I & s | UsedI*Loc I = t | UsedI*Loc I & (for m st m < n holds IC Comput(P,s,m) in dom I) holds (for m st m < n holds IC Comput(Q,t,m) in dom I) & for m st m <= n holds IC Comput(P,s,m) = IC Comput(Q,t,m) & (for a st a in UsedILoc I holds Comput(P,s,m).a = Comput(Q,t,m).a) & for f st f in UsedI*Loc I holds Comput(P,s,m).f = Comput(Q,t,m).f; reserve i1 for Instruction of SCM+FSA; theorem :: SF_MASTR:66 for I being MacroInstruction of SCM+FSA, k being Nat holds UsedILoc(I ';' goto k) = UsedILoc I; theorem :: SF_MASTR:67 for I being MacroInstruction of SCM+FSA, k being Nat holds UsedI*Loc(I ';' goto k) = UsedI*Loc I;