Re: [isabelle] Is Simpl code executable?
Am 28/03/2012 15:56, schrieb Christine Sherif Rizkallah:
> Dear Tobias,
> Thanks for the clarification.
> I guess what I am looking for is a way to limit the Simpl programs I write to
> those programs from which C code could be generated.
> I guess maybe a way to do that would be just to write C0 code and generate the
> Simpl code. The only drawback of this is that I'm not sure how elegant the
> generated Simpl code would be and how easy it would be to verify it.
I would hope you have a good intution which Simpl programs have C0 counterparts
and which do not. In Simpl, expressions can be arbitrary legal HOL expressions,
and of course that contains a lot more than C0.
To be on the safe side, starting from a C0 program seems very reasonable. If
some hand-written Simple program is much easier to verify than a similar
converted C0 program, then you have taken unfair advantage of the expressiveness
of Simpl (or the converter is terrible).
> On Tue, Mar 27, 2012 at 10:34 AM, Tobias Nipkow <nipkow at in.tum.de
> <mailto:nipkow at in.tum.de>> wrote:
> Possibly, Simpl is executable via its operational semantics. But that is
> probably not what you mean. Generating a C program from certain Simpl programs
> should be possible, but I am not sure if anybody has tried this.
> Am 26/03/2012 12:38, schrieb Christine Sherif Rizkallah:
> > Hi all,
> > I'm wondering if anyone knows whether Simpl code is executable.
> > I am new at using Simpl and noticed that I can express
> > things that I cannot express in other imperative languages.
> > For example, assigning variables to functions defined in
> > isabelle (which are in general not necessarily even computable)
> > or setting the conditions of while loops or if statements to
> > boolean expressions starting with "exists or forall".
> > I'm wondering how one can be sure that the Simpl code they
> > write is executable (without automatically parsing it from an
> > imperative language like C).
> > Best,
> > Christine
This archive was generated by a fusion of
Pipermail (Mailman edition) and