Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] How to verify properties of simple SML programs


view this post on Zulip Email Gateway (Oct 02 2021 at 09:19):

From: "N. Raghavendra" <nyraghu27132@gmail.com>
I am using Isabelle for the first time. I would like to verify
properties of simple SML programs. For example, I have an SML file
with the following content:

-- foo.sml

fun foldr _ y [] = y
| foldr f y (x :: xs) = f (x, (foldr f y xs))

fun foldl _ y [] = y
| foldl f y (x :: xs) = foldl f (f (x, y)) xs

-- end of file

I am able to import this SML from an Isabelle file like this

-- foo.thy

theory foo
imports Pure
begin

SML_file ‹foo.sml›

end

-- end of file

Now how do I prove, e.g., that

foldl f y xs = foldr f y (rev xs)

Thanks!

Raghu.

view this post on Zulip Email Gateway (Oct 02 2021 at 09:25):

From: Jakub Kądziołka <kuba@kadziolka.net>
The workflow of producing a verified program in Isabelle goes the other
way around — you define the functions in your Isabelle code, and then
instruct Isabelle to generate the corresponding code in SML, OCaml,
Haskell, or Scala, by using the export_code command (see
https://isabelle.in.tum.de/dist/Isabelle2021/doc/codegen.pdf).

The SML_file command imports your definitions on the meta level — they
can be used to write automation for finding the proofs, but are
completely outside of the logic and nothing can be proved about them.

Hope this helps.

Regards,
Jakub Kądziołka

view this post on Zulip Email Gateway (Oct 03 2021 at 05:15):

From: "N. Raghavendra" <nyraghu27132@gmail.com>
Thanks for the clarification. I'll see the program extraction manual.

Regards,
Raghu.


At 2021-10-02T11:20:12+02:00, Jakub Kądziołka wrote:

view this post on Zulip Email Gateway (Oct 03 2021 at 05:17):

From: "N. Raghavendra" <nyraghu27132@gmail.com>
At 2021-10-02T13:35:27+02:00, Buday Gergely István wrote:

If you wanted to verify ML programs you might take a look at CakeML
where you can verify ML programs down to machine code using HOL4.

Thanks for the pointer. It seems a bit far from my interests now.

Regards,
Raghu.


Last updated: Dec 08 2021 at 08:24 UTC