Re: [isabelle] Hoare-Logic-bubble_Sort

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!

From: mahmoud abdelazim
Date: 2014-11-28 17:39
To: cl-isabelle-users
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
  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 ) 

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