Share Your Experience: Take the 2024 Developer Survey

# Tag Info

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 ...
• 161k

### 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 ...
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 ...
• 277k
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
• 2,553

### 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 ...
• 5,694

### 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 ...
• 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 (...
• 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, ...
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 ...
• 277k
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 ...
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....
• 111

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