Re: [isabelle] Hoare-Logic-bubble_Sort



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

> On 01.12.2014, at 22:56, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
>
> 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
>>>
>>
>
>


________________________________

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.


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