ADT SpecificationCaml [  ]

INITIALS
valSpec: String*TypeExprCaml ->SpecificationCaml
typeSpec:  TypeDefCaml -> SpecificationCaml
exceptionSpec:ExceptionDefCaml ->SpecificationCaml
directiveSpec:DirectiveCaml->SpecificationCaml

CONSTRUCTORS

SELECTORS
StringOfSpecificationCaml: SpecificationCaml(i)  -> String
EQ_SpecificationCaml(c): SpecificationCaml(i) * SpecificationCaml(i)  -> BOOL

AXIOMS

StringOfSpecificationCaml(valSpec(S1,T2))=
  concat_String("val ",
  concat_String(S1,
  concat_String(":",StringOfTypeExprCaml(T2))))
StringOfSpecificationCaml(typeSpec(T1))=StringOfTypeDefCaml(T1)
StringOfSpecificationCaml(exceptionSpec(E1))=StringOfExceptionDefCaml(E1)
StringOfSpecificationCaml(directiveSpec(D1))=StringOfDirectiveCaml(D1)

EQ_SpecificationCaml(valSpec(S1,T2),valSpec(S3,T4))=EQ_String(S1,S3)
EQ_SpecificationCaml(valSpec(S1,T2),typeSpec(T3))=       FALSE
EQ_SpecificationCaml(valSpec(S1,T2),exceptionSpec(E3))=  FALSE
EQ_SpecificationCaml(valSpec(S1,T2),directiveSpec(D3))=  FALSE
EQ_SpecificationCaml(typeSpec(T1),valSpec(S2,T3))=       FALSE
EQ_SpecificationCaml(typeSpec(T1),typeSpec(T2))=EQ_TypeDefCaml(T1,T2)
EQ_SpecificationCaml(typeSpec(T1),exceptionSpec(E2))=    FALSE
EQ_SpecificationCaml(typeSpec(T1),directiveSpec(D2))=    FALSE
EQ_SpecificationCaml(exceptionSpec(E1),valSpec(S2,T3))=  FALSE
EQ_SpecificationCaml(exceptionSpec(E1),typeSpec(T2))=    FALSE
EQ_SpecificationCaml(exceptionSpec(E1),exceptionSpec(E2))=
  EQ_ExceptionDefCaml(E1,E2)
EQ_SpecificationCaml(exceptionSpec(E1),directiveSpec(D2))=FALSE
EQ_SpecificationCaml(directiveSpec(D1),valSpec(S2,T3))=   FALSE
EQ_SpecificationCaml(directiveSpec(D1),typeSpec(T2))=     FALSE
EQ_SpecificationCaml(directiveSpec(D1),exceptionSpec(E2))=FALSE
EQ_SpecificationCaml(directiveSpec(D1),directiveSpec(D2))=
  EQ_DirectiveCaml(D1,D2)