Specification and development of functional programs

This module contains the basic definitions of the program specification and data refinement framework and the definitions of some basic specification operations. See (##luorefinement ##luorefinement)(##luotypetheoryforcs ##luotypetheoryforcs, 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