Premium
LETOS – a lightweight execution tool for operational semantics
Author(s) -
Hartel Pieter H.
Publication year - 1999
Publication title -
software: practice and experience
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.437
H-Index - 70
eISSN - 1097-024X
pISSN - 0038-0644
DOI - 10.1002/(sici)1097-024x(19991225)29:15<1379::aid-spe286>3.0.co;2-v
Subject(s) - computer science , haskell , programming language , operational semantics , compiler , laziness , rendering (computer graphics) , semantics (computer science) , formal semantics (linguistics) , java , software engineering , functional programming , artificial intelligence , psychology , psychiatry
A lightweight tool is proposed to aid in the development of operational semantics. To use LETOS an operational semantics must be expressed in its meta‐language, which itself is a superset of Miranda. The LETOS compiler is smaller than comparable tools, yet LETOS is powerful enough to support publication quality rendering using LaTeX, fast enough to provide competitive execution using Haskell, and versatile enough to support browsing of execution traces using Netscape. LETOS can be characterised as an experiment in ‘creative laziness’, showing how far one can get by gluing existing components together. The major specifications built using LETOS to‐date are a smart card version of the Java Virtual Machine, a deterministic version of the π‐calculus, and an electronic payment protocol. In addition, we have specified the semantics of many small programming languages and systems, totaling over 9000 lines of formal text. LETOS is unique in that it helps to check that a specification is operationally conservative. Copyright © 1999 John Wiley & Sons, Ltd.