*To*: Christian Sternagel <c.sternagel at gmail.com>*Subject*: Re: [isabelle] Hoare-Logic-bubble_Sort*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Mon, 1 Dec 2014 11:56:28 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <547C3197.3060900@gmail.com>*References*: <039B2A5B-F6E3-4091-851A-DD09A9405973@icloud.com> <2014120112221711178220@ios.ac.cn> <547C3197.3060900@gmail.com>

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 >> >

**Follow-Ups**:**Re: [isabelle] Hoare-Logic-bubble_Sort***From:*Gerwin Klein

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

**Re: [isabelle] Hoare-Logic-bubble_Sort***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] Hoare-Logic-bubble_Sort
- Next by Date: Re: [isabelle] thin_tac
- 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