(* //===========================================================================
-- //
-- // AUTHOR(S): Wishnu Prasetya, Ade Azurat
-- // PACKAGE  : (c)xMECH, class LITE, version alpha 1.3.1
-- //
-- //======================================================================== *)
(* // *)
(* =================================================================

This HOL Script will prove the swapArray program specified in the file
swapArray.spec.

================================================================= *)

val litemechDir = "../../hollib" ;

loadPath := !loadPath @ [litemechDir] ;
use  (litemechDir ^ "/litemech.smx") ;

(* === [1] proof of the abstracted total correctness *)

val std_tac =
	REMOVE_MARKER_TAC
	THEN REMOVE_PSEUDO_CONST_TAC
	THEN REPEAT CONJ_TAC
	THEN RW_TAC std_ss []
	THEN TRY ( mesonLib.GEN_MESON_TAC 2 2 8 [])
	THEN TRY COOPER_TAC
	THEN RW_TAC std_ss array_thms ;

read_mechout "swapArray.ls.hout.std" ;
val std_vc = snd from_mech ; 
print "\n\n==>[1] Verification of abstracted standard correctness.... \n\n" ;
val justification_of_stdcor_bls_spec = (Count.apply prove) (std_vc, std_tac) ;

(* -------------------------------------------------------------
Run data:
runtime: 0.321s,    gctime: 0.070s,     systime: 0.321s.
Axioms asserted: 0.
Definitions made: 0.
Oracle invocations: 0.
Theorems loaded from disk: 0.
HOL primitive inference steps: 1522.
Total: 1522.
------------------------------------------------------------- *)

(* ==[2] proof of array overflow check *)

read_mechout "swapArray.ls.hout.aoc" ;
val aoc_vc = snd from_mech ; 

print "\n\n==>[2] Verification of array overflow check....\n\n" ;

val justification_of_aoc_bls_spec = (Count.apply prove) 
	(aoc_vc, 
	 REMOVE_MARKER_TAC
	 THEN REMOVE_PSEUDO_CONST_TAC
	 THEN RW_TAC std_ss array_thms ) ;


(* -------------------------------------------------------------
Run data:
runtime: 0.191s,    gctime: 0.010s,     systime: 0.191s.
Axioms asserted: 0.
Definitions made: 0.
Oracle invocations: 0.
Theorems loaded from disk: 0.
HOL primitive inference steps: 229.
Total: 229.
------------------------------------------------------------- *)

(* ==[3] proof of division by zero is skipped; goal is trivial 
   (program does not contain any division operation) *)

print "\n\n==>[3] Verification of division by zero check is skipped (trivial). \n\n" ;

print "\n\n==> DONE. \n\n" ;

(* END *)