Quasi-Boolean Encodings and Conditionals in Algebraic
Specification
(abstract)
We develop a general study of the algebraic specification practice, originating
from the OBJ tradition, which encodes atomic sentences in logical specification
languages as Boolean terms.
This practice originally motivated by operational aspects, but also leading to
significant increase in expressivity power, has recently become important
within the context of some formal verification methodologies mainly because
it allows the use of simple equational reasoning for frameworks based on logics
that do not have an equational nature.
Our development includes a generic rigorous definition of the logics underlying
the above mentioned practice, based on the novel concept of `quasi-Boolean
encoding', a general result on existence of initial semantics for these logics,
and presents a general method for employing Birkhoff calculus of conditional
equations as a sound calculus for these logics.
The high level of generality of our study means that the concepts are introduced
and the results are obtained at the level of abstract institutions (in the
sense of Goguen and Burstall \cite{ins}) and are therefore applicable to a
multitude of logical systems and environments.
back to Selected Publications