Stack Overflow
Stack Overflow

Questions tagged [hoare-logic]

hoare-logic is a formal system for demonstrating the correctness of programs

What is it?

Hoare-logic is a formal system for demonstrating the correctness of programs.

It uses tripples that express a relation between a pre-condition, a command and a post-condition, and uses a set of axioms and inference rules to draw conclusions on the programme.

See also

52 questions
5
votes
3 answers

Is {true} x := y { x = y } a valid Hoare triple?

I am not sure that { true } x := y { x = y } is a valid Hoare triple. I am not sure one is allowed to reference a variable (in this case, y), without explicitly defining it first either in the triple program body or in the pre-condition. { y=1 } x…
devoured elysium
  • 101,373
  • 131
  • 340
  • 557
5
votes
1 answer

How can I prove this binary search algorithm is correct using hoare logic?

This is the algorithm: // Precondition: n > 0 l = -1; r = n; while (l+1 != r) { m = (l+r)/2; // I && m == (l+r)/2 if (a[m] <= x) { l = m; } else { r = m; } } // Postcondition: -1 <= l < n I have done some…
Marcos Pereira
  • 1,169
  • 14
  • 23
5
votes
1 answer

Program verification in Python

I'm teaching a course on FOL and program verification inspired by the book Mordechai Ben-Ari, Mathematical Logic for Computer Science, Springer, 1993-2012. I would like to illustrate notions by having the students program in Python. For FOL I am…
yannis
  • 819
  • 1
  • 9
  • 26
5
votes
2 answers

Explanation of Hoare Partitioning algorithm

As per the pseudo-code given in many websites, I have written this Hoare partitioning algorithm, which takes an array, the start and end indexes of the sub-array to be partitioned based on the pivot given. It works fine, but can somebody explain the…
SexyBeast
  • 7,913
  • 28
  • 108
  • 196
3
votes
1 answer

Does Python provide support for Assumptions as pre-conditions?

Assumptions in Python unit tests Does Python provide support for Assumptions to be used as pre-conditions for tests similar to those provided by JUnit with assumeThat(...) methods for Java. This is important, because of the application of Hoare…
Martin of Hessle
  • 394
  • 3
  • 12
3
votes
1 answer

Quick sort, Hoare partitioning, using random pivot

Other than below, is there a better way to do quick sort using random pivot(I could not do without a swap)? Please advise int hoare_par (int *a, int b, int e) { if (b < e) { int p_i = __random(b, e); __swap(&a[b], &a[p_i]) …
codey modey
  • 983
  • 2
  • 10
  • 23
3
votes
1 answer

Verification condition of an if-else and while loop in Z3

I'm learning Z3 and want to input some verification condition as stated by the Hoare logic and obtain a model of the given Hoare triples. So far I have only been able to verify assignments, here is an example (just to check if I'm doing it…
puma91
  • 336
  • 6
  • 15
3
votes
2 answers

Correctness of Hoare Partition

Hoare partition as given in cormen: Hoare-Partition(A, p, r) x = A[p] i = p - 1 j = r + 1 while true repeat j = j - 1 until A[j] <= x repeat i = i + 1 until A[i] >= x if i < j swap( A[i], A[j] ) else …
hm5
  • 65
  • 5
3
votes
1 answer

What is the relationship between loop invariant and weakest precondition

Given a loop invariant, Wikipedia lists, a nice way to produce the weakest preconditions for a loop (from http://en.wikipedia.org/wiki/Predicate_transformer_semantics): wp(while E inv I do S, R) = I \wedge \forall y. ((E \wedge I) \implies…
Jove
  • 33
  • 4
3
votes
6 answers

Difference between two types of iterations

This is a core question please don't say with regard to syntax or semantics, the question is that what is the actual difference between WHILE loop and FOR loop, everything written in for loop can be done with while loop then why two…
cc4re
  • 4,821
  • 3
  • 20
  • 27
3
votes
4 answers

Hoare partitioning falls into infinite loop

I am trying to write a Hoare partitioning function that takes an array as input, and partitions it with the first element as pivot (I know it's not a good idea, I should be using randomized pivots, like the median-of-medians approach). Problem is…
SexyBeast
  • 7,913
  • 28
  • 108
  • 196
3
votes
1 answer

Proving correctness in formal logic

I was wondering if anyone could help me answer this question. It is from a previous exam paper and I could do with knowing the answer ready for this years exam. This question seems so simple that I am getting completely lost, what exactly is it…
Paul Blundell
  • 1,857
  • 4
  • 22
  • 27
2
votes
2 answers

Hoare Logic, while loop with '<= '

I'm working on some Hoare logic and I am wondering whether my approach is the right one. I have the following program P: s = 0 i = 1 while (i <= n) { s = s + i i = i + 1 } It should satisfy the hoare triple {n >= 0}P{s = n*(n+1)/2} (so it…
bambinoh
  • 63
  • 1
  • 6
2
votes
2 answers

Why partial correctness instead of total correctness?

In Hoare logic, one often makes a distinction between partial and total correctness. Partial correctness means that the program fulfills its specification, or does not terminate (infinite loop or recursion). Does anyone know why this subtlety about…
V. Semeria
  • 3,128
  • 1
  • 10
  • 25
2
votes
1 answer

Hoare partition not working when more than one value is equal to pivot

I'm trying to write my own hoare partition function to better understand it. I thought I followed its definition and pseudo-code well but even though it seems to work as expected on many occasions, it falls apart and goes into infinite loop when a…
MadRabbit
  • 2,460
  • 2
  • 17
  • 18
1
2 3 4