Re: [isabelle] Hoare-Logic-bubble_Sort



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


> On 1 Dec 2014, at 09:15, Christian Sternagel <c.sternagel at gmail.com> wrote:
> 
> 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
> 
> 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.
>> 
>> 
>> 
>> Best regard!
>> 
>> 
>> 
>> 
>> 
>> lyj238
>> 
>> From: mahmoud abdelazim
>> Date: 2014-11-28 17:39
>> To: cl-isabelle-users
>> Subject: [isabelle] Hoare-Logic-bubble_Sort
>> 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
>> 
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.