Types, subtypes, and ASL+

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

ASL+ is a formalism for specification and programming in-the-large, based on an arbitrary institution. It has rules for proving the satisfaction and refinement of specifications, which can be seen as a type theory with subtyping, including contravariant refinement for II-abstracted specifications and a notion of stratified equality for higher-order objects. We describe the syntax of the language and a partial equivalence relation semantics. This style of semantics is familiar from subtyping calculi, but a novelty here is the use of a hierarchy of typed domains instead of a single untyped domain. We introduce the formal system for proving satisfaction and refinement and describe how it is linked to proof systems of the underlying programming and specification languages.
Original languageEnglish
Title of host publicationRecent Trends in Data Type Specification
Subtitle of host publication10th Workshop on Specification of Abstract Data Types Joint with the 5th COMPASS Workshop S. Margherita, Italy, May 30 – June 3, 1994 Selected Papers
EditorsEgidio Astesiano, Gianna Reggio, Andrzej Tarlecki
PublisherSpringer Berlin Heidelberg
Pages116-131
Number of pages16
Volume906
ISBN (Electronic)978-3-540-49198-9
ISBN (Print)978-3-540-59132-0
DOIs
Publication statusPublished - 1995

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume906

Fingerprint

Dive into the research topics of 'Types, subtypes, and ASL+'. Together they form a unique fingerprint.

Cite this