The ABCs of Specification: AsmL, Behavior, and Components

We show how to use AsmL, an executable specification language, to provide behavioral interfaces for components. This allows clients to fully understand the meaning of an implementation without access to the source code. AsmL implements the concept of behavioral subtyping to ensure the substitutability of components and provides many advanced specification features such as generic types, transactional semantics, invariants and history constraints.