Typical Examples of Atoment Language Using

Abstract

Atoment is a domain-specific language of executable specifications, used to describe methods and techniques of program verification. In this paper a collection of typical examples of the use of the Atoment language, covering topics such as program models, operational, transformational and axiomatic semantics, formal specification of programming languages is presented.

Keywords

• verification
• specification
• operational semantics
• axiomatic semantics
• transformational semantics
• domain-specific languages
• verification systems