Re: [isabelle] Is Simpl code executable?

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.


On Tue, Mar 27, 2012 at 10:34 AM, Tobias Nipkow <nipkow at> 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.
> Tobias
> 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 MHonArc.