:: The SCMPDS Computer and the Basic Semantics of Its Instructions :: by JingChao Chen :: :: Received June 15, 1999 :: Copyright (c) 1999-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 NUMBERS, SUBSET_1, STRUCT_0, AMI_1, AMI_2, FUNCT_7, SCMPDS_1, RELAT_1, FINSEQ_1, CARD_1, XBOOLE_0, TARSKI, FSM_1, CAT_1, AMI_3, INT_1, XXREAL_0, FUNCT_1, COMPLEX1, ARYTM_3, GRAPHSP, ARYTM_1, NAT_1, FUNCOP_1, FUNCT_4, GLIB_000, SCMPDS_2, MEMSTR_0, GOBRD13, PARTFUN1; notations TARSKI, XBOOLE_0, ENUMSET1, XTUPLE_0, SUBSET_1, XCMPLX_0, RELAT_1, PARTFUN1, FUNCT_1, FUNCT_2, INT_1, ORDINAL1, NAT_1, FUNCOP_1, CARD_1, STRUCT_0, FUNCT_4, FUNCT_7, FINSEQ_1, FINSEQ_4, NUMBERS, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, AMI_2, AMI_3, INT_2, XXREAL_0, SCMPDS_I, SCMPDS_1; constructors DOMAIN_1, REAL_1, FINSEQ_4, AMI_3, SCMPDS_1, RELSET_1, FUNCT_7, NAT_D, VALUED_0; registrations XBOOLE_0, SETFAM_1, RELAT_1, ORDINAL1, FUNCOP_1, XREAL_0, INT_1, CARD_3, AMI_2, FUNCT_1, FUNCT_2, EXTPRO_1, AMI_3, MEASURE6, COMPOS_0, SCM_INST, SCMPDS_I, XTUPLE_0; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: The SCMPDS Computer reserve x for set, k for Element of NAT; definition func SCMPDS -> strict AMI-Struct over Segm 2 equals :: SCMPDS_2:def 1 AMI-Struct(# SCM-Memory,In(NAT,SCM-Memory), SCMPDS-Instr, SCM-OK,SCM-VAL,SCMPDS-Exec#); end; registration cluster SCMPDS -> non empty; end; registration cluster SCMPDS -> with_non-empty_values IC-Ins-separated; end; reserve s for State of SCMPDS; ::$CT theorem :: SCMPDS_2:2 IC SCMPDS = NAT; begin :: The Memory Structure registration cluster Int-like for Object of SCMPDS; end; definition mode Int_position is Int-like Object of SCMPDS; ::$CD end; ::$CT 2 theorem :: SCMPDS_2:5 for l being Int_position holds Values l = INT; begin :: The Instruction Structure reserve d1,d2,d3,d4,d5 for Element of SCM-Data-Loc, k1,k2,k3,k4,k5,k6 for Integer; reserve I for Instruction of SCMPDS; theorem :: SCMPDS_2:6 for I being Instruction of SCMPDS holds InsCode I <= 14; registration let s be State of SCMPDS, d be Int_position; cluster s.d -> integer; end; definition let m,n be Integer; func DataLoc(m,n) -> Int_position equals :: SCMPDS_2:def 3 [1,|.m+n.|]; end; theorem :: SCMPDS_2:7 [14,{},<*k1*>] in SCMPDS-Instr; theorem :: SCMPDS_2:8 [1,{},<*d1*>] in SCMPDS-Instr; theorem :: SCMPDS_2:9 x in { 2,3 } implies [x,{},<*d2,k2*>] in SCMPDS-Instr; theorem :: SCMPDS_2:10 x in { 4,5,6,7,8 } implies [x,{},<*d2,k3,k4*>] in SCMPDS-Instr; theorem :: SCMPDS_2:11 x in { 9,10,11,12,13 } implies [x,{},<*d4,d5,k5,k6*>] in SCMPDS-Instr; reserve a,b,c for Int_position; definition let k1 be Integer; func goto k1 -> Instruction of SCMPDS equals :: SCMPDS_2:def 4 [14,{},<*k1*>]; end; definition let a; func return a -> Instruction of SCMPDS equals :: SCMPDS_2:def 5 [1,{},<*a*>]; end; definition let a; let k1 be Integer; func a := k1 -> Instruction of SCMPDS equals :: SCMPDS_2:def 6 [2,{},<*a,k1*>]; func saveIC(a,k1) -> Instruction of SCMPDS equals :: SCMPDS_2:def 7 [3,{},<*a,k1*>]; end; definition let a; let k1,k2 be Integer; func (a,k1)<>0_goto k2 -> Instruction of SCMPDS equals :: SCMPDS_2:def 8 [4,{},<*a,k1,k2*>]; func (a,k1)<=0_goto k2 -> Instruction of SCMPDS equals :: SCMPDS_2:def 9 [5,{},<*a,k1,k2*>]; func (a,k1)>=0_goto k2 -> Instruction of SCMPDS equals :: SCMPDS_2:def 10 [6,{},<*a,k1,k2*>]; func (a,k1) := k2 -> Instruction of SCMPDS equals :: SCMPDS_2:def 11 [7,{},<*a,k1,k2*>]; func AddTo(a,k1,k2) -> Instruction of SCMPDS equals :: SCMPDS_2:def 12 [8,{},<*a,k1,k2*>]; end; definition let a,b; let k1,k2 be Integer; func AddTo(a,k1,b,k2) -> Instruction of SCMPDS equals :: SCMPDS_2:def 13 [9,{},<*a,b,k1,k2*>]; func SubFrom(a,k1,b,k2) -> Instruction of SCMPDS equals :: SCMPDS_2:def 14 [10,{},<*a,b,k1,k2*>]; func MultBy(a,k1,b,k2) -> Instruction of SCMPDS equals :: SCMPDS_2:def 15 [11,{},<*a,b,k1,k2*>]; func Divide(a,k1,b,k2) -> Instruction of SCMPDS equals :: SCMPDS_2:def 16 [12,{},<*a,b,k1,k2*>]; func (a,k1) := (b,k2) -> Instruction of SCMPDS equals :: SCMPDS_2:def 17 [13,{},<*a,b,k1,k2*>]; end; theorem :: SCMPDS_2:12 InsCode (goto k1) = 14; theorem :: SCMPDS_2:13 InsCode (return a) = 1; theorem :: SCMPDS_2:14 InsCode (a := k1) = 2; theorem :: SCMPDS_2:15 InsCode (saveIC(a,k1)) = 3; theorem :: SCMPDS_2:16 InsCode ((a,k1)<>0_goto k2) = 4; theorem :: SCMPDS_2:17 InsCode ((a,k1)<=0_goto k2) = 5; theorem :: SCMPDS_2:18 InsCode ((a,k1)>=0_goto k2) = 6; theorem :: SCMPDS_2:19 InsCode ((a,k1) := k2) = 7; theorem :: SCMPDS_2:20 InsCode (AddTo(a,k1,k2)) = 8; theorem :: SCMPDS_2:21 InsCode (AddTo(a,k1,b,k2)) = 9; theorem :: SCMPDS_2:22 InsCode (SubFrom(a,k1,b,k2)) = 10; theorem :: SCMPDS_2:23 InsCode (MultBy(a,k1,b,k2)) = 11; theorem :: SCMPDS_2:24 InsCode (Divide(a,k1,b,k2)) = 12; theorem :: SCMPDS_2:25 InsCode ((a,k1) := (b,k2)) = 13; theorem :: SCMPDS_2:26 for ins being Instruction of SCMPDS st InsCode ins = 14 holds ex k1 st ins = goto k1; theorem :: SCMPDS_2:27 for ins being Instruction of SCMPDS st InsCode ins = 1 holds ex a st ins = return a; theorem :: SCMPDS_2:28 for ins being Instruction of SCMPDS st InsCode ins = 2 holds ex a,k1 st ins = a := k1; theorem :: SCMPDS_2:29 for ins being Instruction of SCMPDS st InsCode ins = 3 holds ex a,k1 st ins = saveIC(a,k1); theorem :: SCMPDS_2:30 for ins being Instruction of SCMPDS st InsCode ins = 4 holds ex a,k1, k2 st ins = (a,k1)<>0_goto k2; theorem :: SCMPDS_2:31 for ins being Instruction of SCMPDS st InsCode ins = 5 holds ex a,k1, k2 st ins = (a,k1)<=0_goto k2; theorem :: SCMPDS_2:32 for ins being Instruction of SCMPDS st InsCode ins = 6 holds ex a,k1, k2 st ins = (a,k1)>=0_goto k2; theorem :: SCMPDS_2:33 for ins being Instruction of SCMPDS st InsCode ins = 7 holds ex a,k1, k2 st ins = (a,k1) := k2; theorem :: SCMPDS_2:34 for ins being Instruction of SCMPDS st InsCode ins = 8 holds ex a,k1, k2 st ins = AddTo(a,k1,k2); theorem :: SCMPDS_2:35 for ins being Instruction of SCMPDS st InsCode ins = 9 holds ex a,b,k1 ,k2 st ins = AddTo(a,k1,b,k2); theorem :: SCMPDS_2:36 for ins being Instruction of SCMPDS st InsCode ins = 10 holds ex a,b, k1,k2 st ins = SubFrom(a,k1,b,k2); theorem :: SCMPDS_2:37 for ins being Instruction of SCMPDS st InsCode ins = 11 holds ex a,b, k1,k2 st ins = MultBy(a,k1,b,k2); theorem :: SCMPDS_2:38 for ins being Instruction of SCMPDS st InsCode ins = 12 holds ex a,b, k1,k2 st ins = Divide(a,k1,b,k2); theorem :: SCMPDS_2:39 for ins being Instruction of SCMPDS st InsCode ins = 13 holds ex a,b, k1,k2 st ins = (a,k1) := (b,k2); theorem :: SCMPDS_2:40 for s being State of SCMPDS, d being Int_position holds d in dom s; theorem :: SCMPDS_2:41 for s being State of SCMPDS holds SCM-Data-Loc c= dom s; theorem :: SCMPDS_2:42 for s being State of SCMPDS holds dom DataPart s = SCM-Data-Loc; theorem :: SCMPDS_2:43 for dl being Int_position holds dl <> IC SCMPDS; theorem :: SCMPDS_2:44 for s1,s2 being State of SCMPDS st IC s1 = IC s2 & (for a being Int_position holds s1.a = s2.a) holds s1 = s2; begin :: Execution semantics of the SCMPDS instructions theorem :: SCMPDS_2:45 Exec( a:=k1, s).IC SCMPDS = IC s + 1 & Exec( a:=k1, s).a = k1 & for b st b <> a holds Exec( a:=k1, s).b = s.b; theorem :: SCMPDS_2:46 Exec((a,k1):=k2, s).IC SCMPDS = IC s + 1 & Exec((a,k1):=k2, s). DataLoc(s.a,k1) = k2 & for b st b <> DataLoc(s.a,k1) holds Exec((a,k1):=k2, s). b = s.b; theorem :: SCMPDS_2:47 Exec((a,k1):=(b,k2), s).IC SCMPDS = IC s + 1 & Exec((a,k1):=(b, k2), s).DataLoc(s.a,k1) = s.DataLoc(s.b,k2) & for c st c <> DataLoc(s.a,k1) holds Exec((a,k1):=(b,k2),s).c = s.c; theorem :: SCMPDS_2:48 Exec(AddTo(a,k1,k2), s).IC SCMPDS = IC s + 1 & Exec(AddTo(a,k1, k2), s).DataLoc(s.a,k1)=s.DataLoc(s.a,k1)+k2 & for b st b <>DataLoc(s.a,k1) holds Exec(AddTo(a,k1,k2), s).b = s.b; theorem :: SCMPDS_2:49 Exec(AddTo(a,k1,b,k2), s).IC SCMPDS = IC s + 1 & Exec(AddTo(a, k1,b,k2), s).DataLoc(s.a,k1) = s.DataLoc(s.a,k1) + s.DataLoc(s.b,k2) & for c st c <> DataLoc(s.a,k1) holds Exec(AddTo(a,k1,b,k2),s).c = s.c; theorem :: SCMPDS_2:50 Exec(SubFrom(a,k1,b,k2), s).IC SCMPDS = IC s + 1 & Exec(SubFrom (a,k1,b,k2), s).DataLoc(s.a,k1) = s.DataLoc(s.a,k1) - s.DataLoc(s.b,k2) & for c st c <> DataLoc(s.a,k1) holds Exec(SubFrom(a,k1,b,k2),s).c = s.c; theorem :: SCMPDS_2:51 Exec(MultBy(a,k1,b,k2), s).IC SCMPDS = IC s + 1 & Exec(MultBy(a ,k1,b,k2), s).DataLoc(s.a,k1) = s.DataLoc(s.a,k1) * s.DataLoc(s.b,k2) & for c st c <> DataLoc(s.a,k1) holds Exec(MultBy(a,k1,b,k2),s).c = s.c; theorem :: SCMPDS_2:52 Exec(Divide(a,k1,b,k2), s).IC SCMPDS = IC s + 1 & (DataLoc(s.a, k1) <> DataLoc(s.b,k2) implies Exec(Divide(a,k1,b,k2), s).DataLoc(s.a,k1) = s. DataLoc(s.a,k1) div s.DataLoc(s.b,k2)) & Exec(Divide(a,k1,b,k2), s).DataLoc(s.b ,k2) = s.DataLoc(s.a,k1) mod s.DataLoc(s.b,k2) & for c st c <> DataLoc(s.a,k1) & c <> DataLoc(s.b,k2) holds Exec(Divide(a,k1,b,k2),s).c = s.c; theorem :: SCMPDS_2:53 Exec(Divide(a,k1,a,k1), s).IC SCMPDS = IC s + 1 & Exec(Divide(a,k1,a, k1), s).DataLoc(s.a,k1) = s.DataLoc(s.a,k1) mod s.DataLoc(s.a,k1) & for c st c <> DataLoc(s.a,k1) holds Exec(Divide(a,k1,a,k1),s).c = s.c; definition let s be State of SCMPDS,c be Integer; func ICplusConst(s,c) -> Element of NAT means :: SCMPDS_2:def 18 ex m be Element of NAT st m = IC s & it = |.m+c.|; end; theorem :: SCMPDS_2:54 Exec(goto k1, s).IC SCMPDS = ICplusConst(s,k1) & for a holds Exec(goto k1, s).a = s.a; theorem :: SCMPDS_2:55 ( s.DataLoc(s.a,k1) <> 0 implies Exec((a,k1)<>0_goto k2, s).IC SCMPDS = ICplusConst(s,k2)) & ( s.DataLoc(s.a,k1) = 0 implies Exec((a,k1) <>0_goto k2, s).IC SCMPDS = IC s + 1 ) & Exec((a,k1)<>0_goto k2, s).b = s.b; theorem :: SCMPDS_2:56 ( s.DataLoc(s.a,k1) <= 0 implies Exec((a,k1)<=0_goto k2, s).IC SCMPDS = ICplusConst(s,k2)) & ( s.DataLoc(s.a,k1) > 0 implies Exec((a,k1) <=0_goto k2, s).IC SCMPDS = IC s + 1 ) & Exec((a,k1)<=0_goto k2, s).b = s.b; theorem :: SCMPDS_2:57 ( s.DataLoc(s.a,k1) >= 0 implies Exec((a,k1)>=0_goto k2, s).IC SCMPDS = ICplusConst(s,k2)) & ( s.DataLoc(s.a,k1) < 0 implies Exec((a,k1) >=0_goto k2, s).IC SCMPDS = IC s + 1 ) & Exec((a,k1)>=0_goto k2, s).b = s.b; theorem :: SCMPDS_2:58 Exec(return a, s).IC SCMPDS = (|.s.DataLoc(s.a,RetIC).|)+2 & Exec(return a, s).a = s.DataLoc(s.a,RetSP) & for b st a <> b holds Exec(return a, s).b = s.b; theorem :: SCMPDS_2:59 Exec(saveIC(a,k1),s).IC SCMPDS = IC s + 1 & Exec(saveIC(a,k1), s).DataLoc(s.a,k1) = IC s & for b st DataLoc(s.a,k1) <> b holds Exec(saveIC(a, k1), s).b = s.b; ::$CT theorem :: SCMPDS_2:61 for k be Integer holds ex s be State of SCMPDS st for d being Int_position holds s.d = k; theorem :: SCMPDS_2:62 for k be Integer,loc be Element of NAT holds ex s be State of SCMPDS st s.NAT=loc & for d being Int_position holds s.d = k; theorem :: SCMPDS_2:63 for I being Instruction of SCMPDS st I = [0,{},{}] holds I is halting; theorem :: SCMPDS_2:64 for I being Instruction of SCMPDS st ex s st Exec(I,s).IC SCMPDS = IC s + 1 holds I is non halting; theorem :: SCMPDS_2:65 a:=k1 is non halting; theorem :: SCMPDS_2:66 (a,k1):=k2 is non halting; theorem :: SCMPDS_2:67 (a,k1):=(b,k2) is non halting; theorem :: SCMPDS_2:68 AddTo(a,k1,k2) is non halting; theorem :: SCMPDS_2:69 AddTo(a,k1,b,k2) is non halting; theorem :: SCMPDS_2:70 SubFrom(a,k1,b,k2) is non halting; theorem :: SCMPDS_2:71 MultBy(a,k1,b,k2) is non halting; theorem :: SCMPDS_2:72 Divide(a,k1,b,k2) is non halting; theorem :: SCMPDS_2:73 k1 <> 0 implies goto k1 is non halting; theorem :: SCMPDS_2:74 (a,k1)<>0_goto k2 is non halting; theorem :: SCMPDS_2:75 (a,k1)<=0_goto k2 is non halting; theorem :: SCMPDS_2:76 (a,k1)>=0_goto k2 is non halting; theorem :: SCMPDS_2:77 return a is non halting; theorem :: SCMPDS_2:78 saveIC(a,k1) is non halting; theorem :: SCMPDS_2:79 for I being set holds I is Instruction of SCMPDS implies I = [0,{},{}] or (ex k1 st I = goto k1) or (ex a st I = return a) or (ex a,k1 st I = saveIC(a,k1)) or (ex a, k1 st I = a:=k1) or (ex a,k1,k2 st I = (a,k1):=k2) or (ex a,k1,k2 st I = (a,k1) <>0_goto k2) or (ex a,k1,k2 st I = (a,k1)<=0_goto k2) or (ex a,k1,k2 st I = (a, k1)>=0_goto k2) or (ex a,b,k1,k2 st I = AddTo(a,k1,k2)) or (ex a,b,k1,k2 st I = AddTo(a,k1,b,k2)) or (ex a,b,k1,k2 st I = SubFrom(a,k1,b,k2)) or (ex a,b,k1,k2 st I = MultBy(a,k1,b,k2)) or (ex a,b,k1,k2 st I = Divide(a,k1,b,k2)) or ex a,b, k1,k2 st I = (a,k1):=(b,k2); :: Poniewaz zostal dodany prawdziwy halt, :: tego lematu nie mozna udowodnic. ::Lm11: for W being Instruction of SCMPDS st W is halting holds W = goto 0 ::proof :: set I = goto 0; :: let W be Instruction of SCMPDS such that ::A1: W is halting; :: assume ::A2: I <> W; :: per cases by Th91; :: suppose :: ex k1 st W=goto k1; :: hence thesis by A1,A2,Th85; :: end; :: suppose :: ex a st W = return a; :: hence thesis by A1,Th89; :: end; :: suppose :: ex a,k1 st W = saveIC(a,k1); :: hence thesis by A1,Th90; :: end; :: suppose :: ex a,k1 st W = a:=k1; :: hence thesis by A1,Th77; :: end; :: suppose :: ex a,k1,k2 st W=(a,k1):=k2; :: hence thesis by A1,Th78; :: end; :: suppose :: ex a,k1,k2 st W = (a,k1)<>0_goto k2; :: hence thesis by A1,Th86; :: end; :: suppose :: ex a,k1,k2 st W = (a,k1)<=0_goto k2; :: hence thesis by A1,Th87; :: end; :: suppose :: ex a,k1,k2 st W = (a,k1)>=0_goto k2; :: hence thesis by A1,Th88; :: end; :: suppose :: ex a,b,k1,k2 st W = AddTo(a,k1,k2); :: hence thesis by A1,Th80; :: end; :: suppose :: ex a,b,k1,k2 st W = AddTo(a,k1,b,k2); :: hence thesis by A1,Th81; :: end; :: suppose :: ex a,b,k1,k2 st W = SubFrom(a,k1,b,k2); :: hence thesis by A1,Th82; :: end; :: suppose :: ex a,b,k1,k2 st W = MultBy(a,k1,b,k2); :: hence thesis by A1,Th83; :: end; :: suppose :: ex a,b,k1,k2 st W = Divide(a,k1,b,k2); :: hence thesis by A1,Th84; :: end; :: suppose :: ex a,b,k1,k2 st W = (a,k1):=(b,k2); :: hence thesis by A1,Th79; :: end; ::end; registration cluster SCMPDS -> halting; end; ::Dopoki sa przeskoki, to jednoznacznosc instrukcji, ktora jest halting :: i tak sie nie uda udowodnic. ::theorem Th92: :: for I being Instruction of SCMPDS st I is halting holds I = halt :: SCMPDS ::proof :: let I be Instruction of SCMPDS; :: assume I is halting; :: then I = goto 0 by Lm11; :: hence thesis by Lm11; ::end; theorem :: SCMPDS_2:80 halt SCMPDS = [0,{},{}]; ::$CT theorem :: SCMPDS_2:82 for i being Element of NAT holds IC SCMPDS <> dl.i; ::$CT theorem :: SCMPDS_2:84 Data-Locations SCMPDS = SCM-Data-Loc; ::$CT theorem :: SCMPDS_2:86 InsCode I = 0 implies Exec(I,s) = s;