Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999 Association of Mizar Users

### The SCMPDS Computer and the Basic Semantics of its Instructions

by
Jing-Chao Chen

MML identifier: SCMPDS_2
[ Mizar article, MML identifier index ]

```environ

vocabulary AMI_1, INT_1, AMI_2, GR_CY_1, SCMPDS_1, RELAT_1, FUNCT_1, BOOLE,
CAT_1, FINSET_1, AMI_3, AMI_5, ORDINAL2, FINSEQ_1, MCART_1, ABSVALUE,
FUNCT_2, CARD_3, ARYTM_1, NAT_1, CQC_LANG, FUNCT_4, SCMPDS_2;
notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ORDINAL2, NUMBERS, XCMPLX_0,
XREAL_0, FUNCT_1, FUNCT_2, INT_1, NAT_1, MCART_1, CQC_LANG, CARD_3,
STRUCT_0, GR_CY_1, RELAT_1, FUNCT_4, FINSET_1, FINSEQ_1, AMI_1, AMI_2,
SCMPDS_1, AMI_3, GROUP_1, AMI_5;
constructors DOMAIN_1, NAT_1, CAT_2, SCMPDS_1, AMI_5, MEMBERED;
clusters INT_1, AMI_1, RELSET_1, AMI_2, CQC_LANG, SCMPDS_1, XBOOLE_0,
FRAENKEL, NAT_1, MEMBERED, NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

begin :: The SCMPDS Computer

reserve x for set,
i,j,k for Nat;
definition
func SCMPDS -> strict AMI-Struct over { INT } equals
:: SCMPDS_2:def 1
AMI-Struct(#NAT,0,SCM-Instr-Loc,Segm 14,
SCMPDS-Instr,SCMPDS-OK,SCMPDS-Exec#);
end;

definition
cluster SCMPDS -> non empty non void;
end;

theorem :: SCMPDS_2:1
(ex k st x = 2*k+2) iff x in SCM-Instr-Loc;

theorem :: SCMPDS_2:2
SCMPDS is data-oriented;

theorem :: SCMPDS_2:3
SCMPDS is definite;

definition
cluster SCMPDS -> IC-Ins-separated data-oriented definite;
end;

theorem :: SCMPDS_2:4
the Instruction-Locations of SCMPDS <> INT &
the Instructions of SCMPDS <> INT &
the Instruction-Locations of SCMPDS <> the Instructions of SCMPDS;

theorem :: SCMPDS_2:5
NAT = { 0 } \/ SCM-Data-Loc \/ SCM-Instr-Loc;

reserve s for State of SCMPDS;

theorem :: SCMPDS_2:6
IC SCMPDS = 0;

theorem :: SCMPDS_2:7
for S being SCMPDS-State st S = s holds IC s = IC S;

begin :: The Memory Structure

definition
mode Int_position -> Object of SCMPDS means
:: SCMPDS_2:def 2
it in SCM-Data-Loc;
end;

canceled;

theorem :: SCMPDS_2:9
x in SCM-Data-Loc implies x is Int_position;

theorem :: SCMPDS_2:10
SCM-Data-Loc misses the Instruction-Locations of SCMPDS;

theorem :: SCMPDS_2:11
the Instruction-Locations of SCMPDS is infinite
;

theorem :: SCMPDS_2:12
for I being Int_position holds I is Data-Location;

theorem :: SCMPDS_2:13
for l being Int_position holds ObjectKind l = INT;

theorem :: SCMPDS_2:14
for x being set st x in SCM-Instr-Loc
holds x is Instruction-Location of SCMPDS;

begin :: The Instruction Structure
reserve
d1,d2,d3,d4,d5 for Element of SCM-Data-Loc,
k1,k2,k3,k4,k5,k6 for Integer;

definition let I be Instruction of SCMPDS;
cluster InsCode I -> natural;
end;

reserve I for Instruction of SCMPDS;

theorem :: SCMPDS_2:15
for I being Instruction of SCMPDS holds InsCode I <= 13;

definition let s be State of SCMPDS, d be Int_position;
redefine func s.d -> Integer;
end;

definition let m,n be Integer;
canceled;

func DataLoc(m,n) -> Int_position equals
:: SCMPDS_2:def 4
2*abs(m+n)+1;
end;

theorem :: SCMPDS_2:16
[0,<*k1*>] in SCMPDS-Instr;

theorem :: SCMPDS_2:17
[1,<*d1*>] in SCMPDS-Instr;

theorem :: SCMPDS_2:18
x in { 2,3 } implies [x,<*d2,k2*>] in SCMPDS-Instr;

theorem :: SCMPDS_2:19
x in { 4,5,6,7,8 } implies [x,<*d3,k3,k4*>] in SCMPDS-Instr;

theorem :: SCMPDS_2:20
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;
func goto k1 -> Instruction of SCMPDS equals
:: SCMPDS_2:def 5
[ 0, <*k1*>];
end;

definition let a;
func return a -> Instruction of SCMPDS equals
:: SCMPDS_2:def 6
[ 1, <*a*>];
end;

definition let a,k1;
func a := k1 -> Instruction of SCMPDS equals
:: SCMPDS_2:def 7
[ 2, <*a,k1*>];

func saveIC(a,k1) -> Instruction of SCMPDS equals
:: SCMPDS_2:def 8
[ 3, <*a,k1*>];
end;

definition let a,k1,k2;
func (a,k1)<>0_goto k2 -> Instruction of SCMPDS equals
:: SCMPDS_2:def 9
[ 4, <*a,k1,k2*>];

func (a,k1)<=0_goto k2 -> Instruction of SCMPDS equals
:: SCMPDS_2:def 10
[ 5, <*a,k1,k2*>];

func (a,k1)>=0_goto k2 -> Instruction of SCMPDS equals
:: SCMPDS_2:def 11
[ 6, <*a,k1,k2*>];

func (a,k1) := k2 -> Instruction of SCMPDS equals
:: SCMPDS_2:def 12
[ 7, <*a,k1,k2*>];

func AddTo(a,k1,k2) -> Instruction of SCMPDS equals
:: SCMPDS_2:def 13
[ 8, <*a,k1,k2*>];
end;

definition let a,b,k1,k2;
func AddTo(a,k1,b,k2) -> Instruction of SCMPDS equals
:: SCMPDS_2:def 14
[ 9, <*a,b,k1,k2*>];

func SubFrom(a,k1,b,k2) -> Instruction of SCMPDS equals
:: SCMPDS_2:def 15
[ 10, <*a,b,k1,k2*>];

func MultBy(a,k1,b,k2) -> Instruction of SCMPDS equals
:: SCMPDS_2:def 16
[ 11, <*a,b,k1,k2*>];

func Divide(a,k1,b,k2) -> Instruction of SCMPDS equals
:: SCMPDS_2:def 17
[ 12, <*a,b,k1,k2*>];

func (a,k1) := (b,k2) -> Instruction of SCMPDS equals
:: SCMPDS_2:def 18
[ 13, <*a,b,k1,k2*>];
end;

theorem :: SCMPDS_2:21
InsCode (goto k1) = 0;

theorem :: SCMPDS_2:22
InsCode (return a) = 1;

theorem :: SCMPDS_2:23
InsCode (a := k1) = 2;

theorem :: SCMPDS_2:24
InsCode (saveIC(a,k1)) = 3;

theorem :: SCMPDS_2:25
InsCode ((a,k1)<>0_goto k2) = 4;

theorem :: SCMPDS_2:26
InsCode ((a,k1)<=0_goto k2) = 5;

theorem :: SCMPDS_2:27
InsCode ((a,k1)>=0_goto k2) = 6;

theorem :: SCMPDS_2:28
InsCode ((a,k1) := k2) = 7;

theorem :: SCMPDS_2:29

theorem :: SCMPDS_2:30

theorem :: SCMPDS_2:31
InsCode (SubFrom(a,k1,b,k2)) = 10;

theorem :: SCMPDS_2:32
InsCode (MultBy(a,k1,b,k2)) = 11;

theorem :: SCMPDS_2:33
InsCode (Divide(a,k1,b,k2)) = 12;

theorem :: SCMPDS_2:34
InsCode ((a,k1) := (b,k2)) = 13;

theorem :: SCMPDS_2:35
for ins being Instruction of SCMPDS st InsCode ins = 0
holds ex k1 st ins = goto k1;

theorem :: SCMPDS_2:36
for ins being Instruction of SCMPDS st InsCode ins = 1
holds ex a st ins = return a;

theorem :: SCMPDS_2:37
for ins being Instruction of SCMPDS st InsCode ins = 2
holds ex a,k1 st ins = a := k1;

theorem :: SCMPDS_2:38
for ins being Instruction of SCMPDS st InsCode ins = 3
holds ex a,k1 st ins = saveIC(a,k1);

theorem :: SCMPDS_2:39
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:40
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:41
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:42
for ins being Instruction of SCMPDS st InsCode ins = 7
holds ex a,k1,k2 st ins = (a,k1) := k2;

theorem :: SCMPDS_2:43
for ins being Instruction of SCMPDS st InsCode ins = 8
holds ex a,k1,k2 st ins = AddTo(a,k1,k2);

theorem :: SCMPDS_2:44
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:45
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:46
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:47
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:48
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:49
for s being State of SCMPDS, d being Int_position
holds d in dom s;

theorem :: SCMPDS_2:50
for s being State of SCMPDS holds SCM-Data-Loc c= dom s;

theorem :: SCMPDS_2:51
for s being State of SCMPDS
holds dom (s|SCM-Data-Loc) = SCM-Data-Loc;

theorem :: SCMPDS_2:52
for dl being Int_position holds
dl <> IC SCMPDS;

theorem :: SCMPDS_2:53
for il being Instruction-Location of SCMPDS,dl being Int_position holds
il <> dl;

theorem :: SCMPDS_2:54
for s1,s2 being State of SCMPDS
st IC s1 = IC s2 &
(for a being Int_position holds s1.a = s2.a) &
for i being Instruction-Location of SCMPDS holds s1.i = s2.i
holds s1 = s2;

definition let loc be Instruction-Location of SCMPDS;
func Next loc -> Instruction-Location of SCMPDS means
:: SCMPDS_2:def 19
ex mj being Element of SCM-Instr-Loc st mj = loc & it = Next mj;
end;

theorem :: SCMPDS_2:55
for loc being Instruction-Location of SCMPDS,
mj being Element of SCM-Instr-Loc st mj = loc
holds Next mj = Next loc;

theorem :: SCMPDS_2:56
for i being Element of SCMPDS-Instr st i = I
for S being SCMPDS-State st S = s holds Exec(I,s) = SCM-Exec-Res(i,S);

begin :: Execution semantics of the SCMPDS instructions

theorem :: SCMPDS_2:57
Exec( a:=k1, s).IC SCMPDS = Next IC s &
Exec( a:=k1, s).a = k1 &
for b st b <> a holds Exec( a:=k1, s).b = s.b;

theorem :: SCMPDS_2:58
Exec((a,k1):=k2, s).IC SCMPDS = Next IC s &
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:59
Exec((a,k1):=(b,k2), s).IC SCMPDS = Next IC s &
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:60
Exec(AddTo(a,k1,k2), s).IC SCMPDS = Next IC s &
for b st b <>DataLoc(s.a,k1) holds Exec(AddTo(a,k1,k2), s).b = s.b;

theorem :: SCMPDS_2:61
Exec(AddTo(a,k1,b,k2), s).IC SCMPDS = Next IC s &
= 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:62
Exec(SubFrom(a,k1,b,k2), s).IC SCMPDS = Next IC s &
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:63
Exec(MultBy(a,k1,b,k2), s).IC SCMPDS = Next IC s &
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:64
Exec(Divide(a,k1,b,k2), s).IC SCMPDS = Next IC s &
(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:65
Exec(Divide(a,k1,a,k1), s).IC SCMPDS = Next IC s &
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) -> Instruction-Location of SCMPDS means
:: SCMPDS_2:def 20
ex m be Nat st m = IC s & it = abs(m-2+2*c)+2;
end;

theorem :: SCMPDS_2:66
Exec(goto k1, s).IC SCMPDS = ICplusConst(s,k1) &
for a holds Exec(goto k1, s).a = s.a;

theorem :: SCMPDS_2:67
( 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 = Next IC s ) &
Exec((a,k1)<>0_goto k2, s).b = s.b;

theorem :: SCMPDS_2:68
( 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 = Next IC s ) &
Exec((a,k1)<=0_goto k2, s).b = s.b;

theorem :: SCMPDS_2:69
( 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 = Next IC s ) &
Exec((a,k1)>=0_goto k2, s).b = s.b;

theorem :: SCMPDS_2:70
Exec(return a, s).IC SCMPDS = 2*(abs(s.DataLoc(s.a,RetIC)) div 2)+4 &
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:71
Exec(saveIC(a,k1),s).IC SCMPDS = Next IC s &
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;

theorem :: SCMPDS_2:72
for k be Integer holds
(ex f being Function of SCM-Data-Loc,INT st
for x being Element of SCM-Data-Loc holds f.x = k );

theorem :: SCMPDS_2:73
for k be Integer holds
(ex s be State of SCMPDS st for d being Int_position holds s.d = k );

theorem :: SCMPDS_2:74
for k be Integer,loc be Instruction-Location of SCMPDS holds
(ex s be State of SCMPDS st s.0=loc &
for d being Int_position holds s.d = k );

theorem :: SCMPDS_2:75
goto 0 is halting;

theorem :: SCMPDS_2:76
for I being Instruction of SCMPDS st
ex s st Exec(I,s).IC SCMPDS = Next IC s
holds I is non halting;

theorem :: SCMPDS_2:77
a:=k1 is non halting;

theorem :: SCMPDS_2:78
(a,k1):=k2 is non halting;

theorem :: SCMPDS_2:79
(a,k1):=(b,k2) is non halting;

theorem :: SCMPDS_2:80

theorem :: SCMPDS_2:81

theorem :: SCMPDS_2:82
SubFrom(a,k1,b,k2) is non halting;

theorem :: SCMPDS_2:83
MultBy(a,k1,b,k2) is non halting;

theorem :: SCMPDS_2:84
Divide(a,k1,b,k2) is non halting;

theorem :: SCMPDS_2:85
k1 <> 0 implies goto k1 is non halting;

theorem :: SCMPDS_2:86
(a,k1)<>0_goto k2 is non halting;

theorem :: SCMPDS_2:87
(a,k1)<=0_goto k2 is non halting;

theorem :: SCMPDS_2:88
(a,k1)>=0_goto k2 is non halting;

theorem :: SCMPDS_2:89
return a is non halting;

theorem :: SCMPDS_2:90
saveIC(a,k1) is non halting;

theorem :: SCMPDS_2:91
for I being set holds I is Instruction of SCMPDS iff
(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));

definition
cluster SCMPDS -> halting;
end;

theorem :: SCMPDS_2:92
for I being Instruction of SCMPDS st I is halting holds I = halt SCMPDS;

theorem :: SCMPDS_2:93
halt SCMPDS = goto 0;

canceled 2;

theorem :: SCMPDS_2:96
for s being State of SCMPDS, i being Instruction of SCMPDS,
l being Instruction-Location of SCMPDS
holds Exec(i,s).l = s.l;

theorem :: SCMPDS_2:97
SCMPDS is realistic;

definition