Email Gateway (Dec 05 2023 at 15:46): Email Gateway (Dec 05 2023 at 15:46):From: riyuejiuzhao <cl-isabelle-users@lists.cam.ac.uk>
Hello everyone
I am a student who has just started to learn about program verification and
Isabelle. Recently, I have been studying how to use Isabelle to verify C
language programs, but I am struggling to find easy-to-understand and
beginner-friendly tutorials.
Currently, I am facing a simple problem, but I don't know how to approach it.
First, I installed Isabelle/C and wrote the following code:
theory CMyTest
imports "../main/C_Main"
begin
C‹
void swap(int *a,int *b){
int c = b;
int *b = *a;
int *a = c;
}
›
end
Next, I want to prove that the swap function can exchange the values of a and
b, but I don't know how to write it. Can you please guide me on how to modify
the code so that Isabelle can achieve my goal?
Thank you very much for your help!
Best regards,
DongZe Su
Email Gateway (Dec 05 2023 at 19:28):From: Alex Weisberger <alex.m.weisberger@gmail.com>
I'm not familiar with Isabelle/C. I have used Autocorres before, this post
has a simple example theorem about destructive array updates in it:
https://concerningquality.com/quality-and-paradigm.
At a high level though, what you want to do is to write a correctness
statement in terms of the Isabelle definition that corresponds to your swap
function, and then prove that proposition. In Autocorres, if you have a C
function named "swap", then you can refer to it via an Isabelle definition
named: "swap'." I'm assuming Isabelle/C has something similar, but again
not sure.
If you switch to Autocorres, you can just write a proposition using swap'.
I might try doing that.
Email Gateway (Dec 05 2023 at 22:52):From: Yutaka Nagashima <united.reasoning@gmail.com>
Hi DongZe,
Maybe this is the document you are looking for?
https://trustworthy.systems/projects/TS/autocorres/quickstart.pdf
Regards,
Yutaka
Blog: https://unitedreasoning.com
Twitter: https://twitter.com/YutakangE
YouTube: https://www.youtube.com/@unitedreasoning6567
GitHub: https://github.com/yutakang
Email Gateway (Dec 08 2023 at 11:20):From: Burkhart Wolff <cl-isabelle-users@lists.cam.ac.uk>
Hi,
Isabelle/C is just a frontend - you will have to choose a backend.
There are two choices: Clean or AutoCorres. For the type of program
you are targeting, I suggest AutoCorres.
If you want to use Isabelle/C/AutoCorres, you’ll best use
The bundle https://zenodo.org/records/6827097#.YwjXci0RqWY
Isabelle21-1 or 22. There is no more recent version of this bundle
At present.
However, there is a pure Isabelle/AutoCorres version (without the
Frontend) available for Isabelle 2023 from the AutoCorres developper page.
Hope that helps,
Burkhart
Email Gateway (Dec 12 2023 at 03:01):From: Christine Rizkallah <cl-isabelle-users@lists.cam.ac.uk>
Hi all,
What is that front end you speak of?
Thanks for that, and here I was thinking the latest release version of Autocorres is for Isabelle2020.
Are the later versions stable and are there any particular AutoCorres commits that could be released for later Isabelle versions?
Thanks,
Christine
Email Gateway (Dec 12 2023 at 14:59):From: Burkhart Wolff <cl-isabelle-users@lists.cam.ac.uk>
Hi
Well, the C < … > - command creates a completely new type of context (besides text-contexts,
ML-contexts and term-contexts, Isabelle/C adds C-contexts to the Isabelle platform) in which
Isabelle behaves like a C-IDE with efficient parsing, high-lighting, and a very basic type-checking.
C-contexts have also their own form of antiquotations inside C-comments, which are user-programmable.
See our FIDE Paper for more details…
https://www.lri.fr/~wolff/papers/conf/2019-fide-isabelle_c.pdf <https://www.lri.fr/~wolff/papers/conf/2019-fide-isabelle_c.pdf>
https://zenodo.org/records/6827097#.YwjXci0RqWY <https://zenodo.org/records/6827097#.YwjXci0RqWY>
Isabelle/C produces internally a C11 AST from which semantic backends can encode
a semantic representation in Isabelle/HOL.
Hope that helps,
Burkhart
Screenshot 2023-12-12 at 04.16.52.png
Email Gateway (Dec 14 2023 at 15:26):From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Will leave the Isabelle/C frontend to Burkhart, but I can confirm that more recent AutoCorres releases are available on Github under https://github.com/seL4/l4v/releases (including for Isabelle2023).
The old website was out of date, I’ve updated it now to point there.
Cheers,
Gerwin
Email Gateway (Dec 22 2023 at 15:57):From: "\"DongZe Su\"" <cl-isabelle-users@lists.cam.ac.uk>
Thanks very much for your help, I have successfully installed c-parser and
autocorres. But in the process of learning autocorres, I found that I did not
know enough about the language used by Isabelle.
I can understand the structure of the examples in the documentation, but I
can't quite understand the language details.
For example:
lemma n1: ‹((a::word32)≤b) = ((-1-a)≥(-1-b))›
apply(subst word_le_def)+
apply (subst word_n1_ge [simplified uint_minus_simple_alt])+
apply arith
done
In the above example, I could guess that "word32" would correspond to the
"unsigned int" in c, and "apply(subst word_le_def)" would apply a theory, but
where these things, "subst" "word_le_def" "uint_minus_simple_alt" and "arith",
are defined? If I write the lemma myself, how am I going to find the theorems
that I need?
Where should I start learning next?
Email Gateway (Dec 26 2023 at 20:51):From: Lawrence Paulson <lp15@cam.ac.uk>
I suggest that you go to the documentation panel and work through "Programming and Proving in Isabelle/HOL”, which is the first item listed. (It can also be downloaded from the Isabelle website.)
To look up individual tokens in your Isabelle theory (while in jEdit), hold down CTRL (CMD on Macs) and move your mouse over some token, then click.
Larry Paulson
Last updated: Apr 28 2024 at 16:17 UTC