Skip to main content
Share Your Experience: Take the 2024 Developer Survey
31 votes
Accepted

Program Correctness, The specification

First off, you're absolutely right: you're on to a real concern. Formal verification transfers the problem of confidence in program correctness to the problem of confidence in specification ...
D.W.'s user avatar
  • 161k
19 votes

Program Correctness, The specification

D.W.'s answer is great, but I'd like to expand on one point. A specification is not just a reference against which the code is verified. One of the reasons to have a formal specification is to ...
Gilles 'SO- stop being evil''s user avatar
6 votes
Accepted

Finding a good loop invariant for a powering procedure

No, you can't say that $power \leq x^n$ is a loop invariant, since it is not maintained by the loop. For example, if $x > 1$ and at the current iteration $power = x^n$, then the invariant is ...
Yuval Filmus's user avatar
3 votes
Accepted

What is this operator in "The Temporal Logic of Programs" Pnueli 1977?

It's implication as indicated in en.wikipedia.org/wiki/List_of_mathematical_symbols
Brent's user avatar
  • 2,553
2 votes

True Postcondition, with true Precondition

A true postcondition means there is no restriction on outputs. Think about it. The condition x > 5 means: it's true (anything goes), as long as ...
reinierpost's user avatar
  • 5,694
2 votes

Would it be possible to run destructors when aborting a thread?

You can abort a C++ thread in such a way that destructors of automatic ("stack") variables are called: just throw an exception that you don't catch (or that you catch only in a ...
benrg's user avatar
  • 2,157
1 vote

Would it be possible to run destructors when aborting a thread?

I agree, this is not how C++ handles thread abortion. I don't think such correctness guarantees can be achieved in C++ without turning to garbage collection (GC) techniques or binary instrumentation (...
Chaos's user avatar
  • 543
1 vote

Prove correctness of the iterative algorithm

Let Nums be the value of the array after method execution, and nums the initial value. Let, ...
Musa Al-hassy's user avatar
1 vote

What is the loop invariant of the following function?

Try finding a loop invariant of the following form: $$ f(x,y) \leq n < g(x,y). $$ For example, when $y=0$ you could choose $f(x,y) = x$ and $g(x,y) = x+1$, and in the end you want this invariant ...
Yuval Filmus's user avatar
1 vote

Finding a good loop invariant for a powering procedure

Let's rewrite your code using a while-loop so that everything is explicit. { 1 ≤ n } i ≔ 0; p ≔ 1; while i < n: i  ≔ i + 1; p ≔ p * x { p ≈ xⁿ } Note that ...
Musa Al-hassy's user avatar
1 vote

Formal program verification in practice

Perhaps, a model checker may be helpful. http://alloytools.org/documentation.html Alloy is a model checker. A nice presentation explaining the concept of model checking using Alloy: https://www....
ticktock's user avatar
  • 111

Only top scored, non community-wiki answers of a minimum length are eligible