:: A Small Computer Model with Push-Down Stack
:: by JingChao Chen
::
:: Received June 15, 1999
:: Copyright (c) 1999-2026 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, CARD_1, AMI_2, INT_1, XBOOLE_0, FINSEQ_1,
RELAT_1, ARYTM_3, FUNCT_1, CARD_3, AMI_1, FUNCOP_1, COMPLEX1, XXREAL_0,
ARYTM_1, ZFMISC_1, FUNCT_5, SCMPDS_1, GROUP_9;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, CARD_1, FUNCT_2,
BINOP_1, ORDINAL1, NUMBERS, XCMPLX_0, CARD_3, INT_1, NAT_1, FINSEQ_1,
FUNCOP_1, XXREAL_0, FUNCT_5, AMI_2, INT_2, COMPOS_0, SCMPDS_I;
constructors NAT_1, NAT_D, FUNCT_5, AMI_2, RELSET_1, FUNCOP_1, COMPOS_0,
SCMPDS_I, BINOP_1;
registrations ORDINAL1, RELSET_1, XREAL_0, INT_1, FINSEQ_1, CARD_3, AMI_2,
FUNCT_1, FUNCT_2, SCM_INST, SCMPDS_I;
requirements NUMERALS, SUBSET, BOOLE;
definitions TARSKI, FINSEQ_1;
theorems AMI_2, FINSEQ_1, TARSKI, FUNCT_1, FUNCT_2, INT_1, XBOOLE_0, XBOOLE_1,
FUNCT_5;
schemes BINOP_1;
begin :: Preliminaries
reserve
i, j, k for Element of NAT,
I,I2,I3,I4 for Element of Segm 15,
i1 for Element of NAT,
d1,d2,d3,d4,d5 for Element of SCM-Data-Loc,
k1,k2 for Integer;
::$CT 2
theorem
for d be Element of SCM-Data-Loc holds d in SCM-Data-Loc \/ INT
by XBOOLE_1:7,TARSKI:def 3;
begin :: The construction of SCM with Push-Down Stack
:: [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
::$CD 5
let s be SCM-State, a be Element of SCM-Data-Loc, n be Integer;
func Address_Add(s,a,n) -> Element of SCM-Data-Loc equals
[1,|.s.a+n.|];
coherence by AMI_2:24;
end;
definition
let s be SCM-State, n be Integer;
func jump_address(s,n) -> Element of NAT equals
|.(IC s qua Element of NAT)+n.|;
coherence;
end;
definition
let d be Element of SCM-Data-Loc, s be Integer;
redefine func <*d,s*> -> FinSequence of SCM-Data-Loc \/ INT; :: redefines <* (FINSEQ_1, definition)
coherence
proof
let y be object;
A1: dom <*d,s*> = {1,2} by FINSEQ_1:2,89;
assume y in rng <*d,s*>;
then consider x being object such that
A2: x in dom <*d,s*> and
A3: <*d,s*>.x = y by FUNCT_1:def 3;
per cases by A2,A1,TARSKI:def 2;
suppose
x = 1;
then y = d by A3;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A4: x = 2;
A5: s in INT by INT_1:def 2;
y = s by A3,A4;
hence thesis by A5,XBOOLE_0:def 3;
end;
end;
end;
definition
::$CD 11
let s be SCM-State, a be Element of SCM-Data-Loc;
func PopInstrLoc(s,a) -> Element of NAT equals
|.s.a.|+2;
coherence;
end;
:: RetSP: Return Stack Pointer
:: RetIC: Return Instruction-Counter
::$CD 2
definition
let x be Element of SCMPDS-Instr, s be SCM-State;
func SCM-Exec-Res (x,s) -> SCM-State equals
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 qua Element of NAT),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;
definition
func SCMPDS-Exec -> Action of SCMPDS-Instr,
product(SCM-VAL*SCM-OK) means
for x being Element of SCMPDS-Instr, y being
SCM-State holds (it.x).y = SCM-Exec-Res (x,y);
existence
proof
consider f being
Function of [:SCMPDS-Instr,product(SCM-VAL*SCM-OK):], product
(SCM-VAL*SCM-OK) such that
A1: for x being Element of SCMPDS-Instr, y being SCM-State holds f.
(x,y) = SCM-Exec-Res(x,y) from BINOP_1:sch 4;
take curry f;
let x be Element of SCMPDS-Instr, y be SCM-State;
thus (curry f).x.y = f.(x,y) by FUNCT_5:69
.= SCM-Exec-Res(x,y) by A1;
end;
uniqueness
proof
let f, g be Action of SCMPDS-Instr, product(SCM-VAL*SCM-OK) such that
A2: for x being Element of SCMPDS-Instr, y being SCM-State holds (f
.x).y = SCM-Exec-Res(x,y) and
A3: for x being Element of SCMPDS-Instr, y being SCM-State holds (g
.x).y = SCM-Exec-Res(x,y);
now
let x be Element of SCMPDS-Instr;
reconsider gx = g.x, fx = f.x
as Function of product(SCM-VAL*SCM-OK), product
(SCM-VAL*SCM-OK) by FUNCT_2:66;
now
let y be SCM-State;
thus fx.y = SCM-Exec-Res(x,y) by A2
.= gx.y by A3;
end;
hence f.x = g.x by FUNCT_2:63;
end;
hence f = g by FUNCT_2:63;
end;
end;