An Algebraic Semantics for Gnome via a Translation to etoile Specifications
Marc Aiguier, Gilles Bernot, Jaime Ramos, Amı́lcar Sernadas · 2008
Gnome is a simplified and revised version of the object oriented specification language Oblog. A formal semantics based on temporal logic has already been defined, and alternative semantics are also being studied. The goal of this article is to propose an algebraic semantics for Gnome, using étoile. étoile is an algebraic theory for the specification of systems, with an object oriented specification style. It allows to specify objects with local states, systems and their in-variants. There is also in étoile a logical system which is sound w.r.t. the algebraic semantics. Given a Gnome specification, we obtain an algebraic semantics for it by translating the Gnome specification into an étoile specification. The main difficulties come from the fact that Gnome is a concrete specification language with built-in primitives whilst étoile is only a specification theory, and also from the way methods are called and executed in Gnome. Proofs can be performed from a Gnome specification using the étoile calculus.