eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2011-04-26
393
408
10.4230/LIPIcs.RTA.2011.393
article
Proving Equality of Streams Automatically
Zantema, Hans
Endrullis, Joerg
Streams are infinite sequences over a given data type. A stream
specification is a set of equations intended to define a stream.
In this paper we focus on equality of streams, more precisely,
for a given set of equations two stream terms are said to be
equal if they are equal in every model satisfying the given
equations. We investigate techniques for proving equality of
streams suitable for automation. Apart from techniques that
were already available in the tool CIRC from Lucanu and Rosu,
we also exploit well-definedness of streams, typically proved
by proving productivity. Moreover, our approach does
not restrict to behavioral input format and does not require
termination.
We present a tool Streambox that can prove equality of a
wide range of examples fully automatically.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol010-rta2011/LIPIcs.RTA.2011.393/LIPIcs.RTA.2011.393.pdf
streams