:: A Small Computer Model with Push-Down Stack
:: by JingChao Chen
::
:: Copyright (c) 1999-2021 Association of Mizar Users

theorem :: SCMPDS_1:1
canceled;

theorem :: SCMPDS_1:2
canceled;

::$CT 2 theorem :: SCMPDS_1:3 for d being Element of SCM-Data-Loc holds d in SCM-Data-Loc \/ INT by ; :: [0,goto L] :: [1,return sp<-sp+0,count<-(sp)+2] :: [2,a:=c(constant)] :: [3,saveIC (a,k)] :: [4,if(a,k)<>0 goto L ] :: [5,if(a,k)<=0 goto L ] :: [6,if(a,k)>=0 goto L ] :: [7,(a,k):=c(constant) ] :: [8,(a,k1)+k2] :: [9, (a1,k1)+(a2,k2)] :: [10,(a1,k1)-(a2,k2)] :: [11,(a1,k1)*(a2,k2)] :: [12,(a1,k1)/(a2,k2)] :: [13,(a1,k1):=(a2,k2)] definition let s be SCM-State; let a be Element of SCM-Data-Loc ; let n be Integer; func Address_Add (s,a,n) -> Element of SCM-Data-Loc equals :: SCMPDS_1:def 6 [1,|.((s . a) + n).|]; coherence [1,|.((s . a) + n).|] is Element of SCM-Data-Loc by AMI_2:24; end; :: deftheorem SCMPDS_1:def 1 : canceled; :: deftheorem SCMPDS_1:def 2 : canceled; :: deftheorem SCMPDS_1:def 3 : canceled; :: deftheorem SCMPDS_1:def 4 : canceled; :: deftheorem SCMPDS_1:def 5 : canceled; :: deftheorem defines Address_Add SCMPDS_1:def 6 : for s being SCM-State for a being Element of SCM-Data-Loc for n being Integer holds Address_Add (s,a,n) = [1,|.((s . a) + n).|]; definition let s be SCM-State; let n be Integer; func jump_address (s,n) -> Element of NAT equals :: SCMPDS_1:def 7 |.((IC s) + n).|; coherence |.((IC s) + n).| is Element of NAT ; end; :: deftheorem defines jump_address SCMPDS_1:def 7 : for s being SCM-State for n being Integer holds jump_address (s,n) = |.((IC s) + n).|; definition let d be Element of SCM-Data-Loc ; let s be Integer; :: original: <* redefine func <*d,s*> -> FinSequence of SCM-Data-Loc \/ INT; coherence proof end; end; definition let s be SCM-State; let a be Element of SCM-Data-Loc ; func PopInstrLoc (s,a) -> Element of NAT equals :: SCMPDS_1:def 19 |.(s . a).| + 2; coherence |.(s . a).| + 2 is Element of NAT ; end; :: deftheorem SCMPDS_1:def 8 : canceled; :: deftheorem SCMPDS_1:def 9 : canceled; :: deftheorem SCMPDS_1:def 10 : canceled; :: deftheorem SCMPDS_1:def 11 : canceled; :: deftheorem SCMPDS_1:def 12 : canceled; :: deftheorem SCMPDS_1:def 13 : canceled; :: deftheorem SCMPDS_1:def 14 : canceled; :: deftheorem SCMPDS_1:def 15 : canceled; :: deftheorem SCMPDS_1:def 16 : canceled; :: deftheorem SCMPDS_1:def 17 : canceled; :: deftheorem SCMPDS_1:def 18 : canceled; :: deftheorem defines PopInstrLoc SCMPDS_1:def 19 : for s being SCM-State for a being Element of SCM-Data-Loc holds PopInstrLoc (s,a) = |.(s . a).| + 2; canceled; canceled; :: RetSP: Return Stack Pointer :: RetIC: Return Instruction-Counter ::$CD 2
definition
let x be Element of SCMPDS-Instr ;
let s be SCM-State;
func SCM-Exec-Res (x,s) -> SCM-State equals :: SCMPDS_1:def 20
SCM-Chg (s,(jump_address (s,()))) if InsCode x = 14
SCM-Chg ((SCM-Chg (s,(),())),((IC s) + 1)) if InsCode x = 2
SCM-Chg ((SCM-Chg (s,(Address_Add (s,(),())),(IC s))),((IC s) + 1)) if InsCode x = 3
SCM-Chg ((SCM-Chg (s,(Address_Add (s,(),())),())),((IC s) + 1)) if InsCode x = 7
otherwise s;
coherence
;
consistency
for b1 being SCM-State holds
;
end;

:: deftheorem defines SCM-Exec-Res SCMPDS_1:def 20 :
for x being Element of SCMPDS-Instr
for s being SCM-State holds

definition
func SCMPDS-Exec -> Action of SCMPDS-Instr,() means :: SCMPDS_1:def 21
for x being Element of SCMPDS-Instr
for y being SCM-State holds (it . x) . y = SCM-Exec-Res (x,y);
existence
ex b1 being Action of SCMPDS-Instr,() st
for x being Element of SCMPDS-Instr
for y being SCM-State holds (b1 . x) . y = SCM-Exec-Res (x,y)
proof end;
uniqueness
for b1, b2 being Action of SCMPDS-Instr,() st ( for x being Element of SCMPDS-Instr
for y being SCM-State holds (b1 . x) . y = SCM-Exec-Res (x,y) ) & ( for x being Element of SCMPDS-Instr
for y being SCM-State holds (b2 . x) . y = SCM-Exec-Res (x,y) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines SCMPDS-Exec SCMPDS_1:def 21 :
for b1 being Action of SCMPDS-Instr,() holds
( b1 = SCMPDS-Exec iff for x being Element of SCMPDS-Instr
for y being SCM-State holds (b1 . x) . y = SCM-Exec-Res (x,y) );