Modeling Systems in CLP with Coinductive Tabling
Joxan Jaffar, Andrew Santosa and Razvan Voicu
Abstract
We present a methodology for the modelling of complex program behavior
in CLP. The first part of this paper is an informal description about
how to represent a system in CLP. At its basic level, this
representation captures the precise trace semantics of concurrent
programs, or even high-level specifications, in the form of a
predicate transformer. Based on traces, the method can also capture
properties of the underlying runtime system such as the scheduler and
the microarchitecture, so as to provide a foundation for reasoning
about resources such as time and space.
The second part of this paper presents a formal and compositional
proof method for reasoning about safety properties of the underlying
system. The idea is that a safety property is simply a CLP goal, and
is proof established by executing the goal by a CLP interpreter.
However, a traditional CLP interpreter does not suffice. We thus
introduce a technique of {\it coinductive tabling} to CLP.
Essentially, this extends CLP so that it can inductively use proof
obligations that are assumed but not yet proven, and it can generate
new proof obligations assertions dynamically.