Re: [isabelle] I/O automata syntax in Isabelle 2011



On Tue, 1 Feb 2011, Giuliano Losa wrote:

the paper "Integrating Theorem Proving and Model Checking in Isabelle/IOA" presents a nice syntax for describing I/O automata and I would like to use it. I found ioa_syn.ML in the Isabelle 2005 distribution but it is not included in later versions. What would it take to make it work in Isabelle 2011?

Essentially a rewrite from scratch, using contemporary Isabelle concepts, and avoiding program-generated strings that are reparsed as terms.

(This IOA specification mechanism dates back to 1999/2000 and was using very old layers of the system, that were gradually phased out after Isabelle2005. The package was never really maintained after its initial implementation, and in recent years it was not even used/tested in the distribution, so it started rotting.)


	Makarius






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.