Tag Info

8

A loop invariant is an expression that is true through all iterations. But it should also lead to the post-condition being true when the loop terminates. Although c-a=1 is true, It doesn't help you in achieving the post-condition. Intuitively, You would want the invariant to be a*N + b = M because that's what division is and that's what guarantees that you'...

7

The loop invariant probably involves the loop control variable. If so, it only makes sense to ask if the invariant is true, when the loop control variable is initialized. When the loop control variable is uninitialized, expressions that involve it are undefined. Consider a simple example, a loop whose purpose is to determine whether all the elements of a (...

7

Just a hint for now, since this is a practice problem: consider a lexicographic combination of orders. In some more detail: Suppose you have two maps $f_1:S\to D_1$ and $f_2:S\to D_2$ from your program states $S$ into well-founded ordered domains $(D_1,\le_1)$ and $(D_2,\le_2)$. The lexicographic combination of $\le_1$ and $\le_2$ is the order $\le$ on $... 6 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 satisfied at the beginning of the loop but not at the end of the loop. Also, this loop invariant doesn't help you prove that at the end$power = x^n$, which is ... 6 What about using a "goal" variable initialized to NIL and taking as invariant "After iteration i, the goal variable contains an index$0 \leq j < i$such that$A[j] = v$if there exists one (in the range$\{0, \cdots, i - 1\}$), or NIL otherwise" ? 5 The word tautology is a technical word. The following is a tautology of classical propositional logic.$\vdash p \lor \neg p$When interpreted over the natural numbers, the following is a theorem.$ (\mathbb{N},<)\vdash \forall x. \exists y. x < y$But we do not say it is a tautology in the strict logical sense of the word because there are ... 5 A Tautology is a formula (in a certain logic) that is true under every model of that logic. That is, it is equivalent to the formula "$True$". A loop invariant, however, is a certain claim that is usually true under some models, and false under others (a model in this case is an algorithm). Then, you prove that the invariant is true under your specific ... 5 You have an intended postcondition for a loop, and you're looking for an interesting invariant. In this scenario, try taking the intended postcondition, and replacing the total number of iterations (here N) by the number of iterations so far (here i). There's no guarantee that this is an invariant: that's only the case if the way the postcondition is somehow ... 5 At the end of each iteration you have $$\forall j: 0 \leq j < i \implies b[j] = a[j+1]$$ which you can prove by induction. Thus, when the algorithm terminates,$i$has reached$n-1$and you have $$\forall j: 0 \leq j < n-1 \implies b[j] = a[j+1]\,.$$ I figured this out by just asking myself what kind of statement I can make at the end of each ... 4 This kind of optimization is more difficult than typical data-flow based transformations, because you need to actually change the branching structure of the control flow graph. You need something more than SSA (or something more than the dataflow graph you get from reaching definitions.) That "something" is the control dependence graph (which relies on ... 4 Generalities Regarding your first question, the correctness of every loop (without fancy control flow!) can always be proven using a loop invariant which states all the possible values of all variables. In your case (or rather in the modification below), this loop invariant would be $$(n,i,r) \in \{(0,0,-1),(0,0,0),(1,0,-1),(1,1,-1),(1,1,1),(2,0,-1),(2,1,-... 4 I am guessing that, by "tautology," you mean a property that is true in all states. (I have seen some Lecturers use the term in that way, e.g., x > 1 \Longrightarrow x > 0, which is true in all states no matter what x is, might be called a "tautology". The technical definition of "tautology" in logic is more narrow, but I will continue to use ... 4 Your invariant, together with the negation of the loop condition, is not strong enough to imply your postcondition. Try adding an additional conjunct to the invariant which, together with \neg\ i<10, implies i=10 (the j=-1 part then follows from i+j=9). 4 There will always be situations where we can see there is a complex invariant but the compiler cannot derive it. Type systems are sound but not complete: not all invariants can be expressed in the type system. So this isn't something specific to Tarjan's algorithm; it is a general fact of life when working in a type system -- sometimes the compiler will ... 3 how do I include the if else statement in the proof? In this example, the if statement describes the basic case and the else statement describes the inductive step. Induction on z. Basis: z = 0.$$ \text{multiply}(y,z) = 0 = y \times 0. $$Induction Hypothesis: Suppose that this algorithm is true when 0 < z < k. Note that we use strong ... 3 As we already know, the loop iteratively calculates the nth Fibonacci number, so it naturally follows that the loop invariant should contain b = \mathsf{fib}(i) condition. But that is not sufficient for us, because the computation depends on the variable a, and we don't need c, because it is initialized in the loop body. The line b ← c + a actually gives ... 3 I think your postcondition is wrong. Since index i is initialized at 0, you're actually summing from 0 to n, not from 1 to n. The postcondition, lets call it P, should be:$$ j = \sum_{k=0}^{n} a[k]$$Or: j = sum(a[0] ... a[n]) Usually you would write$B$as$i \neq n+1$instead of$i \le n$, because it makes the proof easier. In that case, you would ... 3 Rather than telling you whether your specific invariants are correct, let me teach you the procedure for how you can check whether your invariants are correct on your own. Basically, you break it down by looking at each chunk of code separately. For each chunk of code, you look at the invariant before it and after it and see whether they're consistent with ... 3 Your understanding is mostly correct. That is a valid loop invariant. It's just a relatively weak one. It is common to find a situation like this, where there are multiple possible loop invariants, some more useful than others. You've found a relatively weak (less useful, less informative) loop invariant. Your real question is: how do I find a loop ... 3 The loop invariant doesn't "guarantee" anything. It is a summary of relevant information you know about the state of the program when it reaches that point. If your loop is e.g.: k = 5; ... for(int i = 0; i < N; i++) { /* Invariant: k = 5 */ ... k = 207; ... frob_very_hard(&k); ... k *= 3; ... k = 5; } at the marked point ... 3 I would not simplify$(2)$at all. Just apply the rules for if, =, and command composition. Use weakening (pre- or post- rules) when convenient to do so. Below, I added an empty else branch for clarity. // (2): (S1 = S2 <=> X = Y \land E = true) // \land \lnot(X != /\ \land Y != /\ \land E = true) if !(X == /\ and Y == /\) // (3a): (2) \... 3$n-j+1$should work as it satisfied the three properties of a bound function. It is definitely an integer valued function as all variables and 1 are integers. Since$j$is increased by 1 in every iteration, the function decreases by 1 each time. For example let's say$n$was 5 and$j$was 4. Then for the first iteration it would be 5-4+1=2, then the second ... 3 Are invariants true at most part of the loop and can be untrue at some part? Invariants hold prior and after each execution of the loop body; there are no requirements for what happens in between its statements. Not only that, I would even say it is quite the norm that invariants are broken during the loop. Fixing them is actually a sort of programming ... 3 By a happy coincidence, people (Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz and Laurent Thery) have completed formally verified implementations of Tarjan's algorithm in various formal systems! The paper, titled "Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle", can be found, e.g. here. One step of proving correctness in these ... 3 Figure out what the value of y is, depending on x, a, and c. Prove that your formula is correct before the first iteration, and prove that if it is true before an iteration then it is also true after the iteration. 3 I think you are really asking a question about the definition of the notion of well-foundedness. I think the notion of loop variants is a bit of a red herring here: I would argue that any reasonable definition of well-foundedness should enable proving that a loop is terminating iff there is a well-founded relation which acts as a variant for it, almost as a ... 2 There isn't a single loop invariant: any property that remains true during the execution of the loop is a loop invariant. For example, “I am not the Pope” is an invariant of this loop, but it is not a useful one. A useful loop invariant is one that helps in proving some property of the program. Here, presumably, the ultimate point of the exercise is to ... 2 Unfortunately, you can't prove partial correctness of your algorithm because it is incorrect. EDIT: The algorithm provided is indeed correct. Aditionally, you can't prove that an algorithm is "inductive". You can prove its correctness by using loop invariants,which are quite similar to mathematical inductions. We must show three things about a loop ... 2 Sure, if the user provides inductive invariants, you can try to check the validity of the verification conditions. However, this remains undecidable, as it requires checking the validity of a formula in first-order logic (with quantifiers and array expressions), and that's undecidable. It might be feasible often enough in practice to be useful, especially ... 2 Note that$x=i!$. Now it's easy to see$y=(i+1)!$and$z=(2i)!$. So$c=\frac{(2i)!}{i!(i+1)!}$, which is the$i$th Catalan number. P.S. Your formula is wrong. The condition of the inner loop is$j=i+m\le2i$, so$m$is from$1$to$i$instead of$2i-1\$ or something.

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