Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Is Simpl code executable?

Email Gateway (Aug 18 2022 at 19:22):

From: Christine Sherif Rizkallah <christine2711987@gmail.com>
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

Email Gateway (Aug 18 2022 at 19:22):

From: Tobias Nipkow <nipkow@in.tum.de>
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

Email Gateway (Aug 18 2022 at 19:23):

From: Tobias Nipkow <nipkow@in.tum.de>
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@in.tum.de
<mailto:nipkow@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

Email Gateway (Aug 18 2022 at 19:23):

From: Christine Sherif Rizkallah <christine2711987@gmail.com>
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.

Best,
Christine

Last updated: Apr 19 2024 at 16:20 UTC