SCMPDS_1: A Small Computer Model with Push-Down Stack

:: A Small Computer Model with Push-Down Stack
:: by JingChao Chen
::
:: Received June 15, 1999
:: 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 XBOOLE_1:7, TARSKI:def 3;

:: [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 by AMI_2:24;

end;

:: deftheorem SCMPDS_1:def 1 :

:: deftheorem SCMPDS_1:def 2 :

:: deftheorem SCMPDS_1:def 3 :

:: deftheorem SCMPDS_1:def 4 :

:: deftheorem SCMPDS_1:def 5 :

:: deftheorem defines Address_Add SCMPDS_1:def 6 :

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).|;

end;

:: deftheorem defines jump_address SCMPDS_1:def 7 :

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;

end;

:: deftheorem SCMPDS_1:def 8 :

:: deftheorem SCMPDS_1:def 9 :

:: deftheorem SCMPDS_1:def 10 :

:: deftheorem SCMPDS_1:def 11 :

:: deftheorem SCMPDS_1:def 12 :

:: deftheorem SCMPDS_1:def 13 :

:: deftheorem SCMPDS_1:def 14 :

:: deftheorem SCMPDS_1:def 15 :

:: deftheorem SCMPDS_1:def 16 :

:: deftheorem SCMPDS_1:def 17 :

:: deftheorem SCMPDS_1:def 18 :

:: deftheorem defines PopInstrLoc SCMPDS_1:def 19 :

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,(x const_INT)))) if InsCode x = 14
SCM-Chg ((SCM-Chg (s,(x P21address),(x P22const))),((IC s) + 1)) if InsCode x = 2
SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P21address),(x P22const))),(IC s))),((IC s) + 1)) if InsCode x = 3
SCM-Chg ((SCM-Chg (s,(x address_1),(s . (Address_Add (s,(x address_1),RetSP))))),(PopInstrLoc (s,(Address_Add (s,(x address_1),RetIC))))) if InsCode x = 1
SCM-Chg (s,(IFEQ ((s . (Address_Add (s,(x P31address),(x P32const)))),0,((IC s) + 1),(jump_address (s,(x P33const)))))) if InsCode x = 4
SCM-Chg (s,(IFGT ((s . (Address_Add (s,(x P31address),(x P32const)))),0,((IC s) + 1),(jump_address (s,(x P33const)))))) if InsCode x = 5
SCM-Chg (s,(IFGT (0,(s . (Address_Add (s,(x P31address),(x P32const)))),((IC s) + 1),(jump_address (s,(x P33const)))))) if InsCode x = 6
SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),(x P33const))),((IC s) + 1)) if InsCode x = 7
SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),((s . (Address_Add (s,(x P31address),(x P32const)))) + (x P33const)))),((IC s) + 1)) if InsCode x = 8
SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),((s . (Address_Add (s,(x P41address),(x P43const)))) + (s . (Address_Add (s,(x P42address),(x P44const))))))),((IC s) + 1)) if InsCode x = 9
SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),((s . (Address_Add (s,(x P41address),(x P43const)))) - (s . (Address_Add (s,(x P42address),(x P44const))))))),((IC s) + 1)) if InsCode x = 10
SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),((s . (Address_Add (s,(x P41address),(x P43const)))) * (s . (Address_Add (s,(x P42address),(x P44const))))))),((IC s) + 1)) if InsCode x = 11
SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),(s . (Address_Add (s,(x P42address),(x P44const)))))),((IC s) + 1)) if InsCode x = 13
SCM-Chg ((SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),((s . (Address_Add (s,(x P41address),(x P43const)))) div (s . (Address_Add (s,(x P42address),(x P44const))))))),(Address_Add (s,(x P42address),(x P44const))),((s . (Address_Add (s,(x P41address),(x P43const)))) mod (s . (Address_Add (s,(x P42address),(x P44const))))))),((IC s) + 1)) if InsCode x = 12
otherwise s;

coherence ;
consistency ;

end;

:: deftheorem defines SCM-Exec-Res SCMPDS_1:def 20 :

definition

func SCMPDS-Exec -> Action of SCMPDS-Instr,(product (SCM-VAL * SCM-OK)) 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);

proof end;

proof end;

end;

:: deftheorem defines SCMPDS-Exec SCMPDS_1:def 21 :