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).

Tobias

> Best,
> Christine
> 
> 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.
> 
>     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.