Formalization in Specware

• Data Flow architecture as a parameterized theory

• Lattice constructions as parameterized theories

  • stack, product lattices

• Terms for signatures, arrays, etc. using ML-style type definitions

  • SigType = ObjectType | ArrTyp | SigPrTy
  • ReturnType = SigType | Void
  • MethodSig = method of (objectClassName, Methodname, seq(SigType), ReturnType)

Previous slide

Next slide

Back to first slide

View graphic version