Re: [isabelle] Hoare-Logic-bubble_Sort
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
of the Isabelle distribution. And a paper about it is available, e.g., here:
On 12/01/2014 05:22 AM, lyj238 wrote:
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.
From: mahmoud abdelazim
Date: 2014-11-28 17:39
Subject: [isabelle] Hoare-Logic-bubble_Sort
i want to proof the correctness of the bubble Sort algoritmo
procedure BubbleSort( A : lista degli elementi da ordinare )
scambio ← true
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 )
This archive was generated by a fusion of
Pipermail (Mailman edition) and