(more file formats available here)
Though still a draft, this short tutorial (20 pp.) provides a very nice introduction to CCSL (the Coalgebraic Class Specification Language).
The tutorial is centered around a stack specification in CCSL, that is later compiled to PVS, and analyzed. A stack implementation is provided (i.e., a model), and the consistency of the specification proved.
Posted to Software-Eng by Ehud Lamm on 4/2/04; 5:30:01 AM