This module contains the basic definitions of the program specification and data refinement framework and the definitions of some basic specification operations. See (Luo, 1993)(Luo, 1994, Chapter 8) for further details of the framework for data refinement.
** Module lib_adt_basics Imports lib_sigma lib_setoid STR = ... : Type $SPEC : Type(SPEC) $make_SPEC : {Str:STR}(Str->Prop)->SPEC $SPEC_elim : {C_SPEC:SPEC->Type} ({Str:STR}{Ax:Str->Prop}C_SPEC (make_SPEC Str Ax))->{z:SPEC}C_SPEC z [[C_SPEC:SPEC->Type] [f_make_SPEC:{Str:STR}{Ax:Str->Prop}C_SPEC (make_SPEC Str Ax)][Str:STR] [Ax:Str->Prop] SPEC_elim C_SPEC f_make_SPEC (make_SPEC Str Ax) ==> f_make_SPEC Str Ax] Str = ... : SPEC->STR Ax = ... : {z:SPEC}(Str z)->Prop Spec = ... : STR->Type Model = ... : SPEC->Type(sigma) Consistent = ... : SPEC->Prop Impl = ... : {S|STR}(Spec S)->(Spec S)->Prop Sat = ... : {SP,SP'|SPEC}((Str SP')->Str SP)->Prop $IMPL1 : SPEC->SPEC->Type(IMPL1) $make_IMPL1 : {SP,SP'|SPEC}{refn:(Str SP')->Str SP}(Sat refn)->IMPL1|SP|SP' $IMPL1_elim : {SP,SP'|SPEC}{C_IMPL1:(IMPL1|SP|SP')->Type} ({refn:(Str SP')->Str SP}{sat:Sat refn} C_IMPL1 (make_IMPL1 refn sat))->{z:IMPL1|SP|SP'}C_IMPL1 z [[SP,SP'|SPEC][C_IMPL1:(IMPL1|SP|SP')->Type] [f_make_IMPL1:{refn:(Str SP')->Str SP}{sat:Sat refn} C_IMPL1 (make_IMPL1 refn sat)][refn:(Str SP')->Str SP][sat:Sat refn] IMPL1_elim C_IMPL1 f_make_IMPL1 (make_IMPL1 refn sat) ==> f_make_IMPL1 refn sat] refn = ... : {SP,SP'|SPEC}(IMPL1|SP|SP')->(Str SP')->Str SP sat = ... : {SP,SP'|SPEC}{z:IMPL1|SP|SP'}Sat (refn z) IMPL = ... : SPEC->SPEC->Type(IMPL1) Extend = ... : {SP:SPEC}{ext_str:(Str SP)->STR} [S'=Sigma (Str SP) ([s:Str SP]ext_str s)](S'->Prop)->SPEC Extend_AxOnly = ... : {SP:SPEC}((Str SP)->Prop)->SPEC Join = ... : {S|STR}(Spec S)->(Spec S)->SPEC Cross = ... : SPEC->SPEC->SPEC SigmaCirc = ... : {SP:SPEC}((Str SP)->SPEC)->SPEC Pi = ... : {SP:SPEC}((Str SP)->SPEC)->SPEC Con = ... : {S,S'|STR}(S'->S)->(Spec S')->Spec S Sel = ... : {S,S'|STR}(S'->S)->(Spec S)->Spec S' Abs = ... : {S|STR}(S->S->Prop)->(Spec S)->Spec S Hide = ... : {S|STR}{SP:SPEC}((Str SP)->S)->SPEC
An example of the the abstract datatype of stacks, with axiomatisation, proofs of congruence properties, and implementation as an array is also included.
** Module lib_adt_array Imports lib_nat lib_adt_basics $Str_ARRAY : STR $make_Str_ARRAY : {Array:Setoid}(dom Array)->(nat->(dom Array)->nat->dom Array)-> ((dom Array)->nat->nat)->Str_ARRAY $Str_ARRAY_elim : {C_Str_ARRAY:Str_ARRAY->Type} ({Array:Setoid}{newarray:dom Array} {assign:nat->(dom Array)->nat->dom Array} {access:(dom Array)->nat->nat} C_Str_ARRAY (make_Str_ARRAY Array newarray assign access))-> {z:Str_ARRAY}C_Str_ARRAY z [[C_Str_ARRAY:Str_ARRAY->Type] [f_make_Str_ARRAY:{Array:Setoid}{newarray:dom Array} {assign:nat->(dom Array)->nat->dom Array} {access:(dom Array)->nat->nat} C_Str_ARRAY (make_Str_ARRAY Array newarray assign access)] [Array:Setoid][newarray:dom Array] [assign:nat->(dom Array)->nat->dom Array][access:(dom Array)->nat->nat] Str_ARRAY_elim C_Str_ARRAY f_make_Str_ARRAY (make_Str_ARRAY Array newarray assign access) ==> f_make_Str_ARRAY Array newarray assign access] Array = ... : Str_ARRAY->Setoid newarray = ... : {z:Str_ARRAY}dom (Array z) assign = ... : {z:Str_ARRAY}nat->(dom (Array z))->nat->dom (Array z) access = ... : {z:Str_ARRAY}(dom (Array z))->nat->nat EqARRAY = ... : Str_ARRAY->Prop AxARRAY1 = ... : Str_ARRAY->Prop AxARRAY2 = ... : Str_ARRAY->Prop Ax_ARRAY = ... : Str_ARRAY->Prop ARRAY = ... : SPEC
** Module lib_adt_stack Imports lib_nat lib_adt_basics eq = ... : {S|Setoid}(dom S)->(dom S)->Prop $Str_STACK : STR $make_Str_STACK : {Stack:Setoid}(dom Stack)->(nat->(dom Stack)->dom Stack)-> ((dom Stack)->dom Stack)->((dom Stack)->nat)->Str_STACK $Str_STACK_elim : {C_Str_STACK:Str_STACK->Type} ({Stack:Setoid}{empty:dom Stack}{push:nat->(dom Stack)->dom Stack} {pop:(dom Stack)->dom Stack}{top:(dom Stack)->nat} C_Str_STACK (make_Str_STACK Stack empty push pop top))-> {z:Str_STACK}C_Str_STACK z [[C_Str_STACK:Str_STACK->Type] [f_make_Str_STACK:{Stack:Setoid}{empty:dom Stack} {push:nat->(dom Stack)->dom Stack}{pop:(dom Stack)->dom Stack} {top:(dom Stack)->nat} C_Str_STACK (make_Str_STACK Stack empty push pop top)][Stack:Setoid] [empty:dom Stack][push:nat->(dom Stack)->dom Stack] [pop:(dom Stack)->dom Stack][top:(dom Stack)->nat] Str_STACK_elim C_Str_STACK f_make_Str_STACK (make_Str_STACK Stack empty push pop top) ==> f_make_Str_STACK Stack empty push pop top] Stack = ... : Str_STACK->Setoid empty = ... : {z:Str_STACK}dom (Stack z) push = ... : {z:Str_STACK}nat->(dom (Stack z))->dom (Stack z) pop = ... : {z:Str_STACK}(dom (Stack z))->dom (Stack z) top = ... : {z:Str_STACK}(dom (Stack z))->nat EqSTACK = ... : Str_STACK->Prop AxSTACK1 = ... : Str_STACK->Prop AxSTACK2 = ... : Str_STACK->Prop AxSTACK3 = ... : Str_STACK->Prop AxSTACK4 = ... : Str_STACK->Prop Ax_STACK = ... : Str_STACK->Prop STACK = ... : SPEC
** Module lib_adt_stack_cong Imports lib_adt_basics lib_adt_stack RespSTACKpush = ... : Str_STACK->Prop RespSTACKpop = ... : Str_STACK->Prop RespSTACKtop = ... : Str_STACK->Prop RespSTACK = ... : Str_STACK->Prop STACK_CONG = ... : SPEC iterate = ... : {A|Type}(A->A)->nat->A->A pop_iterate = ... : {S:Str STACK_CONG}(Ax STACK_CONG S)->{s:dom (Stack S)}{x:nat} eq (iterate (pop S) (suc x) s) (iterate (pop S) x (pop S s)) pop_iterate_resp = ... : {S:Str STACK_CONG}(Ax STACK_CONG S)->{s,s':dom (Stack S)}(eq s s')-> {x:nat}eq (iterate (pop S) x s) (iterate (pop S) x s') pop_iterate_empty = ... : {S:Str STACK_CONG}(Ax STACK_CONG S)->{i:nat} eq (iterate (pop S) i (empty S)) (empty S) pop_iterate_push = ... : {S:Str STACK_CONG}(Ax STACK_CONG S)->{s:dom (Stack S)}{k,m:nat} eq (iterate (pop S) (suc k) (push S m s)) (iterate (pop S) k s)
** Module lib_adt_list_stack Imports lib_list_basics lib_adt_stack_cong listStack = ... : Str_STACK eqStackL = ... : EqSTACK listStack axStack1L = ... : AxSTACK1 listStack axStack2L = ... : AxSTACK2 listStack axStack3L = ... : AxSTACK3 listStack axStack4L = ... : AxSTACK4 listStack listStack_correct = ... : Ax_STACK listStack respStackL = ... : RespSTACK listStack listStack_correct_cong = ... : Ax STACK_CONG listStack
** Module lib_adt_stack_by_array Imports lib_nat_Lt lib_adt_stack lib_adt_array refnSA = ... : (Str ARRAY)->Str STACK equivSTACK = ... : {A:Str ARRAY}Equivalence (eq|(Stack (refnSA A))) axSTACK1 = ... : {A:Str ARRAY}AxSTACK1 (refnSA A) axSTACK2 = ... : {A:Str ARRAY}AxSTACK2 (refnSA A) axSTACK3 = ... : {A:Str ARRAY}(Ax ARRAY A)->AxSTACK3 (refnSA A) axSTACK4 = ... : {A:Str ARRAY}(Ax ARRAY A)->AxSTACK4 (refnSA A) sat_refnSA = ... : Sat refnSA