begin
begin
set D = Data-Locations ;
set SAt = Start-At (0,SCM+FSA);
theorem Th3:
for
P being
Instruction-Sequence of
SCM+FSA for
S being
State of
SCM+FSA for
I,
J being
Program of
SCM+FSA st
I is_halting_on Initialized S,
P &
J is_halting_on IExec (
I,
P,
S),
P &
I is_closed_on Initialized S,
P &
J is_closed_on IExec (
I,
P,
S),
P holds
I ";" J is_halting_on Initialized S,
P
Lm1:
for p being Instruction-Sequence of SCM+FSA
for I being good Program of SCM+FSA
for J being Program of SCM+FSA
for s being State of SCM+FSA st s . (intloc 0) = 1 & I is_halting_on s,p & J is_halting_on IExec (I,p,s),p & I is_closed_on s,p & J is_closed_on IExec (I,p,s),p & Initialize ((intloc 0) .--> 1) c= s & I ";" J c= p holds
( IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = card I & DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = DataPart (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) & Reloc (J,(card I)) c= p & (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) . (intloc 0) = 1 & p halts_on s & LifeSpan (p,s) = ((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),(Initialized (Result ((p +* I),s))))) & ( J is good implies (Result (p,s)) . (intloc 0) = 1 ) )
theorem Th5:
for
p being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
J being
Program of
SCM+FSA for
Ig being
good Program of
SCM+FSA st
Ig is_halting_on Initialized s,
p &
J is_halting_on IExec (
Ig,
p,
s),
p &
Ig is_closed_on Initialized s,
p &
J is_closed_on IExec (
Ig,
p,
s),
p holds
LifeSpan (
(p +* (Ig ";" J)),
(Initialized s))
= ((LifeSpan ((p +* Ig),(Initialized s))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Result ((p +* Ig),(Initialized s))))))
theorem Th6:
for
p being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
J being
Program of
SCM+FSA for
Ig being
good Program of
SCM+FSA st
Ig is_halting_on Initialized s,
p &
J is_halting_on IExec (
Ig,
p,
s),
p &
Ig is_closed_on Initialized s,
p &
J is_closed_on IExec (
Ig,
p,
s),
p holds
IExec (
(Ig ";" J),
p,
s)
= (IExec (J,p,(IExec (Ig,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig)),SCM+FSA))
theorem Th7:
for
p being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
J being
Program of
SCM+FSA for
Ig being
good Program of
SCM+FSA for
a being
Int-Location st (
Ig is
parahalting or (
Ig is_halting_on Initialized s,
p &
Ig is_closed_on Initialized s,
p ) ) & (
J is
parahalting or (
J is_halting_on IExec (
Ig,
p,
s),
p &
J is_closed_on IExec (
Ig,
p,
s),
p ) ) holds
(IExec ((Ig ";" J),p,s)) . a = (IExec (J,p,(IExec (Ig,p,s)))) . a
theorem Th8:
for
p being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
J being
Program of
SCM+FSA for
Ig being
good Program of
SCM+FSA for
f being
FinSeq-Location st (
Ig is
parahalting or (
Ig is_halting_on Initialized s,
p &
Ig is_closed_on Initialized s,
p ) ) & (
J is
parahalting or (
J is_halting_on IExec (
Ig,
p,
s),
p &
J is_closed_on IExec (
Ig,
p,
s),
p ) ) holds
(IExec ((Ig ";" J),p,s)) . f = (IExec (J,p,(IExec (Ig,p,s)))) . f
theorem
for
p being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
J being
Program of
SCM+FSA for
Ig being
good Program of
SCM+FSA st (
Ig is
parahalting or (
Ig is_halting_on Initialized s,
p &
Ig is_closed_on Initialized s,
p ) ) & (
J is
parahalting or (
J is_halting_on IExec (
Ig,
p,
s),
p &
J is_closed_on IExec (
Ig,
p,
s),
p ) ) holds
DataPart (IExec ((Ig ";" J),p,s)) = DataPart (IExec (J,p,(IExec (Ig,p,s))))
begin
begin
definition
let N,
result be
Int-Location;
func Fib_macro (
N,
result)
-> Program of
SCM+FSA equals
((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))) ";" (Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) ";" (N := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))));
correctness
coherence
((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))) ";" (Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) ";" (N := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))))) is Program of SCM+FSA;
;
end;
::
deftheorem defines
Fib_macro SFMASTR1:def 5 :
for N, result being Int-Location holds Fib_macro (N,result) = ((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))) ";" (Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) ";" (N := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))));
:: local variable
:: set aux = 1-stRWNotIn UsedIntLoc swap(result, next);
:: for the control variable of Times, must not be changed by swap
:: set N_save = 2-ndRWNotIn UsedIntLoc swap(result, next);
:: for saving and restoring N
:: - requires: N <> result
:: - does not change N
:: - note: Times allocates no memory