:: On a Mathematical Model of Programs :: by Yatsuka Nakamura and Andrzej Trybulec :: :: Received December 29, 1992 :: Copyright (c) 1992-2021 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, XBOOLE_0, CARD_1, ZFMISC_1, FINSEQ_1, FUNCT_1, CARD_3, RELAT_1, AMI_1, NAT_1, FUNCT_4, FUNCOP_1, INT_1, ARYTM_3, ARYTM_1, XXREAL_0, FUNCT_5, TARSKI, AMI_2, GROUP_9, PBOOLE, AFINSQ_1, PARTFUN1, ORDINAL1; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, CARD_1, PARTFUN1, NUMBERS, XCMPLX_0, CARD_3, RELAT_1, FUNCT_1, FUNCT_2, PBOOLE, AFINSQ_1, XXREAL_0, BINOP_1, MCART_1, INT_1, FUNCOP_1, FUNCT_4, CAT_2, FINSEQ_1, FUNCT_5, SCM_INST; constructors DOMAIN_1, CAT_2, CARD_3, ABIAN, RELSET_1, AFINSQ_1, VALUED_1, SCM_INST, FUNCT_5, XTUPLE_0, FUNCT_4, NUMBERS; registrations XBOOLE_0, FUNCOP_1, NUMBERS, XXREAL_0, XREAL_0, INT_1, CARD_3, FINSET_1, ORDINAL2, CARD_1, FUNCT_1, RELSET_1, FUNCT_2, AFINSQ_1, SCM_INST, RELAT_1, PBOOLE; requirements NUMERALS, SUBSET, BOOLE; begin :: A small concrete machine reserve x,y,z for set; :: Na razie potrzebny w SCM_INST ::definition :: func SCM-Data-Loc equals :: [:{1},NAT:]; :: coherence; ::end; definition func SCM-Memory -> set equals :: AMI_2:def 1 {NAT} \/ SCM-Data-Loc; end; registration cluster SCM-Memory -> non empty; end; definition redefine func SCM-Data-Loc -> Subset of SCM-Memory; end; ::registration :: cluster SCM-Data-Loc -> non empty; :: coherence; ::end; reserve I,J,K for Element of Segm 9, i,a,a1,a2 for Nat, b,b1,b2,c,c1 for Element of SCM-Data-Loc; definition ::$CD 2 func SCM-OK -> Function of SCM-Memory, Segm 2 means :: AMI_2:def 4 for k being Element of SCM-Memory holds (k = NAT implies it.k = 0) & (k in SCM-Data-Loc implies it.k = 1); end; ::$CT definition func SCM-VAL -> ManySortedSet of Segm 2 equals :: AMI_2:def 5 <%NAT,INT%>; end; ::$CT 4 theorem :: AMI_2:6 (SCM-VAL*SCM-OK).NAT = NAT; theorem :: AMI_2:7 for i being Element of SCM-Memory holds i in SCM-Data-Loc implies (SCM-VAL*SCM-OK).i = INT; registration cluster SCM-VAL*SCM-OK -> non-empty; end; definition mode SCM-State is Element of product(SCM-VAL*SCM-OK); end; theorem :: AMI_2:8 for a being Element of SCM-Data-Loc holds (SCM-VAL*SCM-OK).a = INT; theorem :: AMI_2:9 pi(product(SCM-VAL*SCM-OK),NAT) = NAT; theorem :: AMI_2:10 for a being Element of SCM-Data-Loc holds pi(product(SCM-VAL*SCM-OK),a) = INT; definition let s be SCM-State; func IC(s) -> Element of NAT equals :: AMI_2:def 6 s.NAT; end; definition let s be SCM-State, u be natural Number; func SCM-Chg(s,u) -> SCM-State equals :: AMI_2:def 7 s +* (NAT .--> u); end; theorem :: AMI_2:11 for s being SCM-State, u being natural Number holds SCM-Chg(s,u).NAT = u; theorem :: AMI_2:12 for s being SCM-State, u being natural Number, mk being Element of SCM-Data-Loc holds SCM-Chg(s,u).mk = s.mk; theorem :: AMI_2:13 for s being SCM-State, u,v being natural Number 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:14 for s being SCM-State, t being Element of SCM-Data-Loc, u being Integer holds SCM-Chg(s,t,u).NAT = s.NAT; theorem :: AMI_2:15 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:16 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; registration let s be SCM-State, a be Element of SCM-Data-Loc; cluster s.a -> integer; end; registration let x,y be ExtReal, a,b be Nat; cluster IFGT(x,y,a,b) -> natural; end; definition ::$CD 5 let x be Element of SCM-Instr, s be SCM-State; func SCM-Exec-Res(x,s) -> SCM-State equals :: AMI_2:def 14 SCM-Chg(SCM-Chg(s, x address_1,s.(x address_2)), IC s + 1) if ex mk, ml being Element of SCM-Data-Loc st x = [1, {}, <*mk, ml*>], SCM-Chg(SCM-Chg(s,x address_1, s.(x address_1)+s.(x address_2)),IC s + 1) if ex mk, ml being Element of SCM-Data-Loc st x = [ 2, {}, <*mk, ml*>], SCM-Chg(SCM-Chg(s,x address_1, s.(x address_1)-s.(x address_2)),IC s + 1) if ex mk, ml being Element of SCM-Data-Loc st x = [ 3, {}, <*mk, ml*>], SCM-Chg(SCM-Chg(s,x address_1, s.(x address_1)*s.(x address_2)),IC s + 1) if ex mk, ml being Element of SCM-Data-Loc st x = [ 4, {}, <*mk, ml*>], SCM-Chg(SCM-Chg( SCM-Chg(s, x address_1, s.(x address_1) div s.(x address_2)), x address_2, s.(x address_1) mod s.(x address_2)),IC s + 1) if ex mk, ml being Element of SCM-Data-Loc st x = [ 5, {}, <*mk, ml*>], SCM-Chg(s,x jump_address) if ex mk being Nat st x = [ 6, <*mk*>, {}], SCM-Chg(s,IFEQ(s.(x cond_address),0,x cjump_address,IC s + 1)) if ex mk being Nat, ml being Element of SCM-Data-Loc st x = [7, <*mk*>, <*ml*>], SCM-Chg(s,IFGT(s.(x cond_address),0,x cjump_address,IC s + 1)) if ex mk being Nat, ml being Element of SCM-Data-Loc st x = [ 8, <*mk*>, <*ml*>] otherwise s; end; definition func SCM-Exec -> Action of SCM-Instr, product(SCM-VAL*SCM-OK) means :: AMI_2:def 15 for x being Element of SCM-Instr, y being SCM-State holds (it.x).y = SCM-Exec-Res(x,y); end; begin :: Addenda :: missing, 2007.07.27, A.T. ::$CT 3 theorem :: AMI_2:20 not NAT in SCM-Data-Loc; ::$CT theorem :: AMI_2:22 NAT in SCM-Memory; theorem :: AMI_2:23 x in SCM-Data-Loc implies ex k being Nat st x = [1,k]; theorem :: AMI_2:24 for k being Nat holds [1,k] in SCM-Data-Loc; ::$CT theorem :: AMI_2:26 for k being Element of SCM-Memory holds k = NAT or k in SCM-Data-Loc; theorem :: AMI_2:27 dom(SCM-VAL*SCM-OK) = SCM-Memory; theorem :: AMI_2:28 for s being SCM-State holds dom s = SCM-Memory; definition let x be set; attr x is Int-like means :: AMI_2:def 16 x in SCM-Data-Loc; end; theorem :: AMI_2:29 for S being SCM-State holds S is total (SCM-Memory)-defined Function;