Re: [isabelle] Is Simpl code executable?



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.