*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Hoare-Logic-bubble_Sort*From*: Christian Sternagel <c.sternagel at gmail.com>*Date*: Mon, 01 Dec 2014 10:15:03 +0100*In-reply-to*: <2014120112221711178220@ios.ac.cn>*References*: <039B2A5B-F6E3-4091-851A-DD09A9405973@icloud.com> <2014120112221711178220@ios.ac.cn>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.2.0

Dear lyj238,

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

**Follow-Ups**:**Re: [isabelle] Hoare-Logic-bubble_Sort***From:*Lawrence Paulson

**References**:**Re: [isabelle] Hoare-Logic-bubble_Sort***From:*lyj238

- Previous by Date: Re: [isabelle] Hoare-Logic-bubble_Sort
- Next by Date: Re: [isabelle] Hoare-Logic-bubble_Sort
- Previous by Thread: Re: [isabelle] Hoare-Logic-bubble_Sort
- Next by Thread: Re: [isabelle] Hoare-Logic-bubble_Sort
- Cl-isabelle-users December 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list