Email Gateway (Aug 19 2022 at 16:33): Email Gateway (Aug 19 2022 at 16:33):From: mahmoud abdelazim <m.abdelazim@icloud.com>
Hi
i want to proof the correctness of the bubble Sort algoritmo
procedure BubbleSort( A : lista degli elementi da ordinare )
scambio ← true
while scambio
scambio ← false
for i ← 0 to length(A)-2 do
if A[i] > A[i+1] then
swap( A[i], A[i+1] )
scambio ← true
There exists any Hoare Logic theory in Isabelle that can i use to proof that algorithm (In particular a Hoare Logic theory in Isabelle that implement Arrays too )
Thanks
Email Gateway (Aug 19 2022 at 16:43):From: lyj238 <lyj238@ios.ac.cn>
Yes, I have a similar question.
In a real-world program verification, functions （or procedures) and array are used frequently, without techniques to handle these features, it is too diffcult to apply theorem proving tehnique.
But I really coudl not find techniques to handle functions and arrays in Isabelle src directory or any public source after many searchings.
Best regard!
lyj238
Email Gateway (Aug 19 2022 at 16:45):From: Christian Sternagel <c.sternagel@gmail.com>
Dear lyj238,
if you didn't find any techniques how to handle functions, then you
didn't look very far. Most of today's theorem proving work with
Isabelle/HOL is based on some kind of function definitions (just
definitions without recursion, primitive recursive functions, and more
general recursive functions whose termination has to be proved).
But I reckon that instead of "function" as I understand it, you might
mean something like "side-effects" and thus functions that are allowed
to modify some kind of state. If that is the case (and also for arrays)
you might want to have a look at Imperative_HOL (which is a theory based
on standard Isabelle/HOL).
The sources can be found in the subdirectory
src/HOL/Imperative_HOL/Imperative_HOL.thy
of the Isabelle distribution. And a paper about it is available, e.g., here:
http://www4.in.tum.de/~krauss/imperative/imperative.pdf
cheers
chris
Email Gateway (Aug 19 2022 at 16:46):From: Lawrence Paulson <lp15@cam.ac.uk>
These and similar questions appear to be connected with program verification projects. Isabelle per se is not a program verifier. Isabelle can be used to verify algorithms expressed in a purely functional style, and program verification tools can be built on top of Isabelle. Unfortunately, I’m not personally familiar with the best references to this sort of work. I hope somebody who is better informed than I am can reply with some links.
Larry Paulson
Email Gateway (Aug 19 2022 at 16:48):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Here are a few links for verification of imperative programs:
SIMPL, a generic imperative language in which you can express a number of ‘real’
programming languages and reason about them: http://afp.sourceforge.net/entries/Simpl.shtml
C-Parser, a translator of C into SIMPL:
http://ssrg.nicta.com.au/software/TS/c-parser/
or
https://github.com/seL4/l4v/tree/master/tools/c-parser for development versions
AutoCorres, a tool on top of C-Parser that makes reasoning more convenient by
abstracting from SIMPL into a functional representation:
http://ssrg.nicta.com.au/projects/TS/autocorres/
or
https://github.com/seL4/l4v/tree/master/tools/autocorresfor development versions
src/HOL/Imperative_HOL in the Isabelle distribution, already mentioned below
There are further formalisations of imperative languages in the Isabelle distribution for demonstrating specific aspects or for learning about the semantics of programming languages.
For learning about the verification of imperative programs, it is best to not start with function calls and arrays, but if that’s what you’re mostly interested in, I’d go with SIMPL and look at its example files. If you want to verify C programs, AutoCorres is currently the tool to use in Isabelle.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Nov 21 2024 at 12:39 UTC