ISSN : 1796-217X
Volume : 1    Issue : 3    Date : September 2006

Incremental Implementation of Syntax Driven Logics
Ignatius Sri Wishnu Brata Prasetya, A. Azurat, Tanja E. J. Vos, and Arthur van Leeuwen
Page(s): 1-13
Full Text:
PDF (512 KB)

This paper describes a technique combining higher order functions, algebraic datat ypes, and
monads to incrementally implement syntax driven logics. Extensions can be compositionally
stacked while the base logic is left unchanged. The technique can furthermore be used to build a
set of weaker logics for light weight verification or to generate validation traces. The paper explains
the technique through an example: a Hoare logic for a simple command language. The example
also shows how exceptions can be treated as an extension, without having to change the underlying

Index Terms
syntax driven logic, algebraic data type, modular logic, verification tool.