The Coalgebraic Class Specification Language CCSL
Дата
Авторы
Rothe,Jan
Tews,Hendrik
Jacobs,Bart
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
This paper presents the Coalgebraic Class Specification Language CCSL that is developed within the loop project on formal methods for object-oriented languages. CCSL allows the (coalgebraic) specification of behavioral types and classes of object-oriented languages. It uses higher-order logic with universal modal operators to restrict the behavior of objects. A front-end to the theorem provers pvs [ORR + 96] and ISABELLE [Pau94] compiles CCSL specifications into the logic of these theorem provers and allows to mechanically reason about the specifications.
Ключевые слова
coalgebra , specification , binary methods , modal logic