:: RELOC semantic presentation

definition

let loc be Instruction-Location of SCM ;
let k be Nat;
func loc + k -> Instruction-Location of SCM means :Def1: :: RELOC:def 1
ex m being Nat st
( loc = il. m & it = il. (m + k) );
existence

proof end;

uniqueness by AMI_3:53;
func loc -' k -> Instruction-Location of SCM means :Def2: :: RELOC:def 2
ex m being Nat st
( loc = il. m & it = il. (m -' k) );
existence

proof end;

uniqueness by AMI_3:53;

end;

:: deftheorem Def1 defines + RELOC:def 1 :

:: deftheorem Def2 defines -' RELOC:def 2 :

theorem Th1: :: RELOC:1

for loc being Instruction-Location of SCM
for k being Nat holds (loc + k) -' k = loc

proof end;

theorem Th2: :: RELOC:2

for l1, l2 being Instruction-Location of SCM
for k being Nat holds
( Start-At (l1 + k) = Start-At (l2 + k) iff Start-At l1 = Start-At l2 )

proof end;

theorem Th3: :: RELOC:3

for l1, l2 being Instruction-Location of SCM
for k being Nat st Start-At l1 = Start-At l2 holds
Start-At (l1 -' k) = Start-At (l2 -' k)

proof end;

definition

let I be Instruction of SCM ;
let k be Nat;
func IncAddr I,k -> Instruction of SCM equals :Def3: :: RELOC:def 3
goto ((((@ I) jump_address ) @ ) + k) if InsCode I = 6
(((@ I) cond_address ) @ ) =0_goto ((((@ I) cjump_address ) @ ) + k) if InsCode I = 7
(((@ I) cond_address ) @ ) >0_goto ((((@ I) cjump_address ) @ ) + k) if InsCode I = 8
otherwise I;
correctness ;

end;

:: deftheorem Def3 defines IncAddr RELOC:def 3 :

theorem :: RELOC:4

for k being Nat holds IncAddr (halt SCM ),k = halt SCM by Def3, AMI_5:37;

theorem Th5: :: RELOC:5

for k being Nat
for a, b being Data-Location holds IncAddr (a := b),k = a := b

proof end;

theorem Th6: :: RELOC:6

for k being Nat
for a, b being Data-Location holds IncAddr (AddTo a,b),k = AddTo a,b

proof end;

theorem Th7: :: RELOC:7

for k being Nat
for a, b being Data-Location holds IncAddr (SubFrom a,b),k = SubFrom a,b

proof end;

theorem Th8: :: RELOC:8

for k being Nat
for a, b being Data-Location holds IncAddr (MultBy a,b),k = MultBy a,b

proof end;

theorem Th9: :: RELOC:9

for k being Nat
for a, b being Data-Location holds IncAddr (Divide a,b),k = Divide a,b

proof end;

theorem Th10: :: RELOC:10

for k being Nat
for loc being Instruction-Location of SCM holds IncAddr (goto loc),k = goto (loc + k)

proof end;

theorem Th11: :: RELOC:11

for k being Nat
for loc being Instruction-Location of SCM
for a being Data-Location holds IncAddr (a =0_goto loc),k = a =0_goto (loc + k)

proof end;

theorem Th12: :: RELOC:12

for k being Nat
for loc being Instruction-Location of SCM
for a being Data-Location holds IncAddr (a >0_goto loc),k = a >0_goto (loc + k)

proof end;

theorem Th13: :: RELOC:13

for I being Instruction of SCM
for k being Nat holds InsCode (IncAddr I,k) = InsCode I

proof end;

theorem Th14: :: RELOC:14

for II, I being Instruction of SCM
for k being Nat st ( InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 ) & IncAddr II,k = I holds
II = I

proof end;

definition

let p be programmed FinPartState of SCM ;
let k be Nat;
func Shift p,k -> programmed FinPartState of SCM means :Def4: :: RELOC:def 4
( dom it = { (il. (m + k)) where m is Nat : il. m in dom p } & ( for m being Nat st il. m in dom p holds
it . (il. (m + k)) = p . (il. m) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Shift RELOC:def 4 :

theorem Th15: :: RELOC:15

for l being Instruction-Location of SCM
for k being Nat
for p being programmed FinPartState of SCM st l in dom p holds
(Shift p,k) . (l + k) = p . l

proof end;

theorem :: RELOC:16

for p being programmed FinPartState of SCM
for k being Nat holds dom (Shift p,k) = { (il + k) where il is Instruction-Location of SCM : il in dom p }

proof end;

theorem :: RELOC:17

for p being programmed FinPartState of SCM
for k being Nat holds dom (Shift p,k) c= the Instruction-Locations of SCM

proof end;

definition

let p be programmed FinPartState of SCM ;
let k be Nat;
func IncAddr p,k -> programmed FinPartState of SCM means :Def5: :: RELOC:def 5
( dom it = dom p & ( for m being Nat st il. m in dom p holds
it . (il. m) = IncAddr (pi p,(il. m)),k ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines IncAddr RELOC:def 5 :

theorem Th18: :: RELOC:18

for p being programmed FinPartState of SCM
for k being Nat
for l being Instruction-Location of SCM st l in dom p holds
(IncAddr p,k) . l = IncAddr (pi p,l),k

proof end;

theorem Th19: :: RELOC:19

for i being Nat
for p being programmed FinPartState of SCM holds Shift (IncAddr p,i),i = IncAddr (Shift p,i),i

proof end;

definition

let p be FinPartState of SCM ;
let k be Nat;
func Relocated p,k -> FinPartState of SCM equals :: RELOC:def 6
((Start-At ((IC p) + k)) +* (IncAddr (Shift (ProgramPart p),k),k)) +* (DataPart p);
correctness ;

end;

:: deftheorem defines Relocated RELOC:def 6 :

theorem Th20: :: RELOC:20

for k being Nat
for p being FinPartState of SCM holds dom (IncAddr (Shift (ProgramPart p),k),k) c= SCM-Instr-Loc

proof end;

theorem Th21: :: RELOC:21

for p being FinPartState of SCM
for k being Nat holds DataPart (Relocated p,k) = DataPart p

proof end;

theorem Th22: :: RELOC:22

for p being FinPartState of SCM
for k being Nat holds ProgramPart (Relocated p,k) = IncAddr (Shift (ProgramPart p),k),k

proof end;

theorem Th23: :: RELOC:23

for k being Nat
for p being FinPartState of SCM holds dom (ProgramPart (Relocated p,k)) = { (il. (j + k)) where j is Nat : il. j in dom (ProgramPart p) }

proof end;

theorem Th24: :: RELOC:24

for p being FinPartState of SCM
for k being Nat
for l being Instruction-Location of SCM holds
( l in dom p iff l + k in dom (Relocated p,k) )

proof end;

theorem Th25: :: RELOC:25

for p being FinPartState of SCM
for k being Nat holds IC SCM in dom (Relocated p,k)

proof end;

theorem Th26: :: RELOC:26

for p being FinPartState of SCM
for k being Nat holds IC (Relocated p,k) = (IC p) + k

proof end;

theorem Th27: :: RELOC:27

for p being FinPartState of SCM
for k being Nat
for loc being Instruction-Location of SCM
for I being Instruction of SCM st loc in dom (ProgramPart p) & I = p . loc holds
IncAddr I,k = (Relocated p,k) . (loc + k)

proof end;

theorem Th28: :: RELOC:28

for p being FinPartState of SCM
for k being Nat holds Start-At ((IC p) + k) c= Relocated p,k

proof end;

theorem Th29: :: RELOC:29

for s being data-only FinPartState of SCM
for p being FinPartState of SCM
for k being Nat st IC SCM in dom p holds
Relocated (p +* s),k = (Relocated p,k) +* s

proof end;

theorem Th30: :: RELOC:30

for k being Nat
for p being autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & Relocated p,k c= s2 holds
p c= s1 +* (s2 | SCM-Data-Loc )

proof end;

theorem Th31: :: RELOC:31

for k being Nat
for s being State of SCM holds Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k))

proof end;

theorem Th32: :: RELOC:32

for INS being Instruction of SCM
for s being State of SCM
for j, k being Nat st IC s = il. (j + k) holds
Exec INS,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))

proof end;

theorem :: RELOC:33

for k being Nat
for p being autonomic FinPartState of SCM st IC SCM in dom p holds
for s being State of SCM st p c= s holds
for i being Nat holds (Computation (s +* (Relocated p,k))) . i = (((Computation s) . i) +* (Start-At ((IC ((Computation s) . i)) + k))) +* (ProgramPart (Relocated p,k))

proof end;

theorem Th34: :: RELOC:34

for k being Nat
for p being autonomic FinPartState of SCM
for s1, s2, s3 being State of SCM st IC SCM in dom p & p c= s1 & Relocated p,k c= s2 & s3 = s1 +* (s2 | SCM-Data-Loc ) holds
for i being Nat holds
( (IC ((Computation s1) . i)) + k = IC ((Computation s2) . i) & IncAddr (CurInstr ((Computation s1) . i)),k = CurInstr ((Computation s2) . i) & ((Computation s1) . i) | (dom (DataPart p)) = ((Computation s2) . i) | (dom (DataPart (Relocated p,k))) & ((Computation s3) . i) | SCM-Data-Loc = ((Computation s2) . i) | SCM-Data-Loc )

proof end;

theorem Th35: :: RELOC:35

for p being autonomic FinPartState of SCM
for k being Nat st IC SCM in dom p holds
( p is halting iff Relocated p,k is halting )

proof end;

theorem Th36: :: RELOC:36

for k being Nat
for p being autonomic FinPartState of SCM st IC SCM in dom p holds
for s being State of SCM st Relocated p,k c= s holds
for i being Nat holds (Computation s) . i = ((((Computation (s +* p)) . i) +* (Start-At ((IC ((Computation (s +* p)) . i)) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))

proof end;

theorem Th37: :: RELOC:37

for k being Nat
for p being FinPartState of SCM st IC SCM in dom p holds
for s being State of SCM st p c= s & Relocated p,k is autonomic holds
for i being Nat holds (Computation s) . i = ((((Computation (s +* (Relocated p,k))) . i) +* (Start-At ((IC ((Computation (s +* (Relocated p,k))) . i)) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)

proof end;

theorem Th38: :: RELOC:38

for p being FinPartState of SCM st IC SCM in dom p holds
for k being Nat holds
( p is autonomic iff Relocated p,k is autonomic )

proof end;

theorem Th39: :: RELOC:39

for p being autonomic halting FinPartState of SCM st IC SCM in dom p holds
for k being Nat holds DataPart (Result p) = DataPart (Result (Relocated p,k))

proof end;

theorem :: RELOC:40

for F being PartFunc of FinPartSt SCM , FinPartSt SCM
for p being FinPartState of SCM st IC SCM in dom p & F is data-only holds
for k being Nat holds
( p computes F iff Relocated p,k computes F )

proof end;