NOMIN_5: Partial Correctness of a Factorial Algorithm

end;

:: deftheorem defines PP_composition NOMIN_5:def 1 :

definition

let D be set ;
let f1, f2, f3, f4 be BinominativeFunction of D;

func PP_composition (f1,f2,f3,f4) -> BinominativeFunction of D equals :: NOMIN_5:def 2
PP_composition ((PP_composition (f1,f2,f3)),f4);

unconditional composition rule for 3 programs

end;

:: deftheorem defines PP_composition NOMIN_5:def 2 :

theorem :: NOMIN_5:1

for D being non empty set
for f1, f2, f3 being BinominativeFunction of D
for p, q, r, w being PartialPredicate of D st <*p,f1,q*> is SFHT of D & <*q,f2,r*> is SFHT of D & <*r,f3,w*> is SFHT of D & <*(PP_inversion q),f2,r*> is SFHT of D & <*(PP_inversion r),f3,w*> is SFHT of D holds
<*p,(PP_composition (f1,f2,f3)),w*> is SFHT of D

proof end;

unconditional composition rule for 4 programs

theorem Th2: :: NOMIN_5:2

for D being non empty set
for f1, f2, f3, f4 being BinominativeFunction of D
for p, q, r, t, w being PartialPredicate of D st <*p,f1,q*> is SFHT of D & <*q,f2,r*> is SFHT of D & <*r,f3,w*> is SFHT of D & <*w,f4,t*> is SFHT of D & <*(PP_inversion q),f2,r*> is SFHT of D & <*(PP_inversion r),f3,w*> is SFHT of D & <*(PP_inversion w),f4,t*> is SFHT of D holds
<*p,(PP_composition (f1,f2,f3,f4)),t*> is SFHT of D

proof end;

theorem Th3: :: NOMIN_5:3

for v, v1 being object
for V, A being set
for d1 being NonatomicND of V,A
for T being TypeSCNominativeData of V,A st A is_without_nonatomicND_wrt V & v in V & v <> v1 & v1 in dom d1 holds
(local_overlapping (V,A,d1,T,v)) . v1 = d1 . v1

proof end;

definition

let x, y be object ;
assume A1: ( x is Complex & y is Complex ) ;

func addition (x,y) -> Complex means :Def3: :: NOMIN_5:def 3
ex x1, y1 being Complex st
( x1 = x & y1 = y & it = x1 + y1 );

proof end;

uniqueness ;

func multiplication (x,y) -> Complex means :Def4: :: NOMIN_5:def 4
ex x1, y1 being Complex st
( x1 = x & y1 = y & it = x1 * y1 );

proof end;

uniqueness ;

end;

:: deftheorem Def3 defines addition NOMIN_5:def 3 :

:: deftheorem Def4 defines multiplication NOMIN_5:def 4 :

definition

let A be set ;
assume A1: A is complex-containing ;
deffunc H₁( object , object ) -> Complex = addition ($1,$2);

func addition A -> Function of [:A,A:],A means :Def5: :: NOMIN_5:def 5
for x, y being object st x in A & y in A holds
it . (x,y) = addition (x,y);

proof end;

proof end;

deffunc H₂( object , object ) -> Complex = multiplication ($1,$2);

func multiplication A -> Function of [:A,A:],A means :Def6: :: NOMIN_5:def 6
for x, y being object st x in A & y in A holds
it . (x,y) = multiplication (x,y);

proof end;

proof end;

end;

:: deftheorem Def5 defines addition NOMIN_5:def 5 :

:: deftheorem Def6 defines multiplication NOMIN_5:def 6 :

definition

let V, A be set ;
let x, y be Element of V;

func addition (A,x,y) -> SCBinominativeFunction of V,A equals :: NOMIN_5:def 7
lift_binary_op ((addition A),x,y);

func multiplication (A,x,y) -> SCBinominativeFunction of V,A equals :: NOMIN_5:def 8
lift_binary_op ((multiplication A),x,y);

end;

:: deftheorem defines addition NOMIN_5:def 7 :

:: deftheorem defines multiplication NOMIN_5:def 8 :

theorem Th4: :: NOMIN_5:4

for V, A being set
for d1 being NonatomicND of V,A
for i, j being Element of V st A is complex-containing & i in dom d1 & j in dom d1 & d1 in dom (addition (A,i,j)) holds
for x, y being Complex st x = d1 . i & y = d1 . j holds
(addition (A,i,j)) . d1 = x + y

proof end;

theorem Th5: :: NOMIN_5:5

for V, A being set
for d1 being NonatomicND of V,A
for i, j being Element of V st A is complex-containing & i in dom d1 & j in dom d1 & d1 in dom (multiplication (A,i,j)) holds
for x, y being Complex st x = d1 . i & y = d1 . j holds
(multiplication (A,i,j)) . d1 = x * y

proof end;

definition

let V, A be set ;
let loc be V -valued Function;

func factorial_loop_body (A,loc) -> SCBinominativeFunction of V,A equals :: NOMIN_5:def 9
PP_composition ((SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))),(SC_assignment ((multiplication (A,(loc /. 4),(loc /. 1))),(loc /. 4))));

end;

:: deftheorem defines factorial_loop_body NOMIN_5:def 9 :

definition

let V, A be set ;
let loc be V -valued Function;

func factorial_main_loop (A,loc) -> SCBinominativeFunction of V,A equals :: NOMIN_5:def 10
PP_while ((PP_not (Equality (A,(loc /. 1),(loc /. 3)))),(factorial_loop_body (A,loc)));

end;

:: deftheorem defines factorial_main_loop NOMIN_5:def 10 :

definition

let V, A be set ;
let loc be V -valued Function;
let val be Function;

func factorial_var_init (A,loc,val) -> SCBinominativeFunction of V,A equals :: NOMIN_5:def 11
PP_composition ((SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1))),(SC_assignment ((denaming (V,A,(val . 2))),(loc /. 2))),(SC_assignment ((denaming (V,A,(val . 3))),(loc /. 3))),(SC_assignment ((denaming (V,A,(val . 4))),(loc /. 4))));

end;

:: deftheorem defines factorial_var_init NOMIN_5:def 11 :

definition

let V, A be set ;
let loc be V -valued Function;
let val be Function;

func factorial_main_part (A,loc,val) -> SCBinominativeFunction of V,A equals :: NOMIN_5:def 12
PP_composition ((factorial_var_init (A,loc,val)),(factorial_main_loop (A,loc)));

end;

:: deftheorem defines factorial_main_part NOMIN_5:def 12 :

definition

let V, A be set ;
let loc be V -valued Function;
let val be Function;
let z be Element of V;

func factorial_program (A,loc,val,z) -> SCBinominativeFunction of V,A equals :: NOMIN_5:def 13
PP_composition ((factorial_main_part (A,loc,val)),(SC_assignment ((denaming (V,A,(loc /. 4))),z)));

end;

:: deftheorem defines factorial_program NOMIN_5:def 13 :

definition

let V, A be set ;
let val be Function;
let n0 be Nat;
let d be object ;

pred valid_factorial_input_pred V,A,val,n0,d means :: NOMIN_5:def 14
ex d1 being NonatomicND of V,A st
( d = d1 & {(val . 1),(val . 2),(val . 3),(val . 4)} c= dom d1 & d1 . (val . 1) = 0 & d1 . (val . 2) = 1 & d1 . (val . 3) = n0 & d1 . (val . 4) = 1 );

end;

:: deftheorem defines valid_factorial_input_pred NOMIN_5:def 14 :

definition

let V, A be set ;
let val be Function;
let n0 be Nat;
defpred S₁[ object ] means valid_factorial_input_pred V,A,val,n0,$1;

func valid_factorial_input (V,A,val,n0) -> SCPartialNominativePredicate of V,A means :Def15: :: NOMIN_5:def 15
( dom it = ND (V,A) & ( for d being object st d in dom it holds
( ( valid_factorial_input_pred V,A,val,n0,d implies it . d = TRUE ) & ( not valid_factorial_input_pred V,A,val,n0,d implies it . d = FALSE ) ) ) );

proof end;

proof end;

end;

:: deftheorem Def15 defines valid_factorial_input NOMIN_5:def 15 :

registration

let V, A be set ;
let val be Function;
let n0 be Nat;

cluster valid_factorial_input (V,A,val,n0) -> total ;

coherence by Def15;

end;

definition

let V, A be set ;
let z be Element of V;
let n0 be Nat;
let d be object ;

pred valid_factorial_output_pred A,z,n0,d means :: NOMIN_5:def 16
ex d1 being NonatomicND of V,A st
( d = d1 & z in dom d1 & d1 . z = n0 ! );

end;

:: deftheorem defines valid_factorial_output_pred NOMIN_5:def 16 :

definition

let V, A be set ;
let z be Element of V;
let n0 be Nat;
set D = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } ;
defpred S₁[ object ] means valid_factorial_output_pred A,z,n0,$1;

func valid_factorial_output (A,z,n0) -> SCPartialNominativePredicate of V,A means :Def17: :: NOMIN_5:def 17
( dom it = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom it holds
( ( valid_factorial_output_pred A,z,n0,d implies it . d = TRUE ) & ( not valid_factorial_output_pred A,z,n0,d implies it . d = FALSE ) ) ) );

proof end;

proof end;

end;

:: deftheorem Def17 defines valid_factorial_output NOMIN_5:def 17 :

definition

let V, A be set ;
let loc be V -valued Function;
let n0 be Nat;
let d be object ;

pred factorial_inv_pred A,loc,n0,d means :: NOMIN_5:def 18
ex d1 being NonatomicND of V,A st
( d = d1 & {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} c= dom d1 & d1 . (loc /. 2) = 1 & d1 . (loc /. 3) = n0 & ex I, S being Nat st
( I = d1 . (loc /. 1) & S = d1 . (loc /. 4) & S = I ! ) );

end;

:: deftheorem defines factorial_inv_pred NOMIN_5:def 18 :

definition

let V, A be set ;
let loc be V -valued Function;
let n0 be Nat;
defpred S₁[ object ] means factorial_inv_pred A,loc,n0,$1;

func factorial_inv (A,loc,n0) -> SCPartialNominativePredicate of V,A means :Def19: :: NOMIN_5:def 19
( dom it = ND (V,A) & ( for d being object st d in dom it holds
( ( factorial_inv_pred A,loc,n0,d implies it . d = TRUE ) & ( not factorial_inv_pred A,loc,n0,d implies it . d = FALSE ) ) ) );

proof end;