Re: [isabelle] Ways to add a checking layer for Theories?



Le Fri, 03 Aug 2012 19:21:29 +0200, Gottfried Barrow <gottfried.barrow at gmx.com> a écrit:

On 8/3/2012 9:15 AM, Yannick Duchêne (Hibou57) wrote:
...I mean kind of style check and design rules check.

As an example, one may want to require all Theories to not contain any partial functions. Is there a way to do this without externally re-parsing and re-interpreting *.thy files? (which would be too error‑prone by the way). Do the Isabelle system have provision to invoke such a layer, feeding it with a structure corresponding to the Theory interpretation?

Yannick,

I'll do the easy part and point out page 14 of prog-prove.pdf:

"...all HOL functions must be total. This simplifies the logic—terms are always defined—but means that recursive functions must terminate."

You probably have other examples in mind, and maybe you're not using HOL.

Not that much, I “imports Main”, and that way it's easy to have a “fun” which does not cover all cases, with no error and just a warning.

--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University






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