Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

### On a Mathematical Model of Programs

by
Yatsuka Nakamura, and
Andrzej Trybulec

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

```environ

vocabulary GR_CY_1, TARSKI, INT_1, BOOLE, FINSEQ_1, NAT_1, FUNCT_1, CARD_3,
RELAT_1, AMI_1, FUNCT_4, CAT_1, MCART_1, ARYTM_1, CQC_LANG, FUNCT_2,
FUNCT_5, AMI_2, FINSEQ_4, ARYTM;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS,
XCMPLX_0, XREAL_0, CARD_3, RELAT_1, FUNCT_1, FUNCT_2, GR_CY_1, DOMAIN_1,
INT_1, NAT_1, CQC_LANG, FRAENKEL, FUNCT_4, CAT_2, FINSEQ_1, FINSEQ_4;
constructors GR_CY_1, DOMAIN_1, NAT_1, CAT_2, FINSEQ_4, AMI_1, MEMBERED,
XBOOLE_0;
clusters SUBSET_1, INT_1, AMI_1, FINSEQ_1, CQC_LANG, RELSET_1, XBOOLE_0,
NAT_1, FRAENKEL, MEMBERED, ZFMISC_1, ORDINAL2;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;

begin :: A small concrete machine

reserve x for set;
reserve i,j,k for Nat;

definition
func SCM-Halt -> Element of Segm 9 equals
:: AMI_2:def 1
0;
end;

definition
func SCM-Data-Loc -> Subset of NAT equals
:: AMI_2:def 2
{ 2*k + 1: not contradiction };
func SCM-Instr-Loc -> Subset of NAT equals
:: AMI_2:def 3
{ 2*k : k > 0 };
end;

definition
cluster SCM-Data-Loc -> non empty;
cluster SCM-Instr-Loc -> non empty;
end;

reserve I,J,K for Element of Segm 9,
a,a1,a2 for Element of SCM-Instr-Loc,
b,b1,b2,c,c1 for Element of SCM-Data-Loc;

definition
func SCM-Instr -> Subset of [: Segm 9, (union {INT} \/ NAT)* :] equals
:: AMI_2:def 4
{ [SCM-Halt,{}] } \/
{ [J,<*a*>] : J = 6 } \/
{ [K,<*a1,b1*>] : K in { 7,8 } } \/
{ [I,<*b,c*>] : I in { 1,2,3,4,5} };
end;

canceled;

theorem :: AMI_2:2
[0,{}] in SCM-Instr;

definition
cluster SCM-Instr -> non empty;
end;

theorem :: AMI_2:3
[6,<*a2*>] in SCM-Instr;

theorem :: AMI_2:4
x in { 7, 8 } implies [x,<*a2,b2*>] in SCM-Instr;

theorem :: AMI_2:5
x in { 1,2,3,4,5} implies [x,<*b1,c1*>] in SCM-Instr;

definition
func SCM-OK -> Function of NAT, {INT} \/ { SCM-Instr, SCM-Instr-Loc } means
:: AMI_2:def 5
it.0 = SCM-Instr-Loc &
for k being Nat holds it.(2*k+1) = INT & it.(2*k+2) = SCM-Instr;
end;

theorem :: AMI_2:6
SCM-Instr-Loc <> INT & SCM-Instr <> INT & SCM-Instr-Loc <> SCM-Instr;

theorem :: AMI_2:7
SCM-OK.i = SCM-Instr-Loc iff i = 0;

theorem :: AMI_2:8
SCM-OK.i = INT iff ex k st i = 2*k+1;

theorem :: AMI_2:9
SCM-OK.i = SCM-Instr iff ex k st i = 2*k+2;

definition
mode SCM-State is Element of product SCM-OK;
end;

theorem :: AMI_2:10
for a being Element of SCM-Data-Loc holds
SCM-OK.a = INT;

theorem :: AMI_2:11
for a being Element of SCM-Instr-Loc holds
SCM-OK.a = SCM-Instr;

theorem :: AMI_2:12
for a being Element of SCM-Instr-Loc,
t being Element of SCM-Data-Loc holds a <> t;

theorem :: AMI_2:13
pi(product SCM-OK,0) = SCM-Instr-Loc;

theorem :: AMI_2:14
for a being Element of SCM-Data-Loc holds
pi(product SCM-OK,a) = INT;

theorem :: AMI_2:15
for a being Element of SCM-Instr-Loc holds
pi(product SCM-OK,a) = SCM-Instr;

definition let s be SCM-State;
func IC(s) -> Element of SCM-Instr-Loc equals
:: AMI_2:def 6
s.0;
end;

definition let s be SCM-State, u be Element of SCM-Instr-Loc;
func SCM-Chg(s,u) -> SCM-State equals
:: AMI_2:def 7
s +* (0 .--> u);
end;

theorem :: AMI_2:16
for s being SCM-State, u being Element of SCM-Instr-Loc
holds SCM-Chg(s,u).0 = u;

theorem :: AMI_2:17
for s being SCM-State, u being Element of SCM-Instr-Loc,
mk being Element of SCM-Data-Loc
holds SCM-Chg(s,u).mk = s.mk;

theorem :: AMI_2:18
for s being SCM-State, u,v being Element of SCM-Instr-Loc
holds SCM-Chg(s,u).v = s.v;

definition let s be SCM-State, t be Element of SCM-Data-Loc, u be Integer;
func SCM-Chg(s,t,u) -> SCM-State equals
:: AMI_2:def 8
s +* (t .--> u);
end;

theorem :: AMI_2:19
for s being SCM-State, t being Element of SCM-Data-Loc, u being Integer
holds SCM-Chg(s,t,u).0 = s.0;

theorem :: AMI_2:20
for s being SCM-State, t being Element of SCM-Data-Loc, u being Integer
holds SCM-Chg(s,t,u).t = u;

theorem :: AMI_2:21
for s being SCM-State, t being Element of SCM-Data-Loc, u being Integer,
mk being Element of SCM-Data-Loc st mk <> t
holds SCM-Chg(s,t,u).mk = s.mk;

theorem :: AMI_2:22
for s being SCM-State, t being Element of SCM-Data-Loc, u being Integer,
v being Element of SCM-Instr-Loc
holds SCM-Chg(s,t,u).v = s.v;

definition let x be Element of SCM-Instr;
given mk, ml being Element of SCM-Data-Loc, I such that
x = [ I, <*mk, ml*>];
func x address_1 -> Element of SCM-Data-Loc means
:: AMI_2:def 9
ex f being FinSequence of SCM-Data-Loc st f = x`2 & it = f/.1;
func x address_2 -> Element of SCM-Data-Loc means
:: AMI_2:def 10
ex f being FinSequence of SCM-Data-Loc st f = x`2 & it = f/.2;
end;

theorem :: AMI_2:23
for x being Element of SCM-Instr, mk, ml being Element of SCM-Data-Loc, I
st x = [ I, <*mk, ml*>]

definition let x be Element of SCM-Instr;
given mk being Element of SCM-Instr-Loc, I such that
x = [ I, <*mk*>];
func x jump_address -> Element of SCM-Instr-Loc means
:: AMI_2:def 11
ex f being FinSequence of SCM-Instr-Loc st f = x`2 & it = f/.1;
end;

theorem :: AMI_2:24
for x being Element of SCM-Instr, mk being Element of SCM-Instr-Loc, I
st x = [ I, <*mk*>]

definition let x be Element of SCM-Instr;
given mk being Element of SCM-Instr-Loc,
ml being Element of SCM-Data-Loc, I such that
x = [ I, <*mk,ml*>];
func x cjump_address -> Element of SCM-Instr-Loc means
:: AMI_2:def 12

ex mk being Element of SCM-Instr-Loc,
ml being Element of SCM-Data-Loc st <*mk,ml*> = x`2 & it = <*mk,ml*>/.1;
func x cond_address -> Element of SCM-Data-Loc means
:: AMI_2:def 13

ex mk being Element of SCM-Instr-Loc,
ml being Element of SCM-Data-Loc st <*mk,ml*> = x`2 & it = <*mk,ml*>/.2;
end;

theorem :: AMI_2:25
for x being Element of SCM-Instr,
mk being Element of SCM-Instr-Loc,
ml being Element of SCM-Data-Loc, I
st x = [ I, <*mk,ml*>]

definition let s be SCM-State, a be Element of SCM-Data-Loc;
cluster s.a -> integer;
end;

definition let D be non empty set; let x,y be real number,
a,b be Element of D;
func IFGT(x,y,a,b) -> Element of D equals
:: AMI_2:def 14
a if x > y
otherwise b;
end;

definition let d be Element of SCM-Instr-Loc;
func Next d -> Element of SCM-Instr-Loc equals
:: AMI_2:def 15
d + 2;
end;

definition let x be Element of SCM-Instr, s be SCM-State;
func SCM-Exec-Res(x,s) -> SCM-State equals
:: AMI_2:def 16
if ex mk, ml being Element of SCM-Data-Loc st x = [ 1, <*mk, ml*>],
if ex mk, ml being Element of SCM-Data-Loc st x = [ 2, <*mk, ml*>],
if ex mk, ml being Element of SCM-Data-Loc st x = [ 3, <*mk, ml*>],
if ex mk, ml being Element of SCM-Data-Loc st x = [ 4, <*mk, ml*>],
SCM-Chg(SCM-Chg(
if ex mk, ml being Element of SCM-Data-Loc st x = [ 5, <*mk, ml*>],
if ex mk being Element of SCM-Instr-Loc st x = [ 6, <*mk*>],
if ex mk being Element of SCM-Instr-Loc,
ml being Element of SCM-Data-Loc st x = [ 7, <*mk,ml*>],
if ex mk being Element of SCM-Instr-Loc,
ml being Element of SCM-Data-Loc st x = [ 8, <*mk,ml*>]
otherwise s;
end;

definition
func SCM-Exec ->
Function of SCM-Instr, Funcs(product SCM-OK, product SCM-OK) means
:: AMI_2:def 17
for x being Element of SCM-Instr, y being SCM-State holds
(it.x).y = SCM-Exec-Res(x,y);
end;

```