Specification and development of functional programs

For detailed documentation, see chapter 8 in [Luo, 1994].

 ** 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 are also included.