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