# Questions tagged [correctness-proof]

290 questions
Filter by
Sorted by
Tagged with
11 views

### Verification conditions for Hoare

I am reading about Hoare logic but I don't really understand the verification conditions part for proving partial correctness. What's happening between step 1 to 2? Why do we ignore the Q := 0 and ...
33 views

54 views

34 views

### Prove that a recursive program satisfies a logic predicate with implication and quantifiers by induction [closed]

i have this program to prove: ...
24 views

### Loop invariant initialisation confusion

Consider the algorithm LastMatch below, which returns the offset (shift) of the last occurrence of the pattern P in text T, or -1 if P does not occur in T: ...
571 views

### Why is this pushdown automaton for some palindromes right?

$B = \{w \in \{0,1\}^* | w^R = w, w \text{ length is odd} \}$ Solution: For example: $111$ should be accepted steps are $q_1 \to q_2$ stack: [$\$$]$q_2 \to q_2$stack:$[\$, 1, 1]$ (using up $11$...
52 views

886 views

### How to prove a greedy algorithm that uses the longest increasing subsequence?

Here is the thing, I am solving an problem, and I think, say, I am pretty sure that I have the correct algorithm but I haven't been able to prove it because of my lack of practice prooving greedy ...
34 views

### Using Hoare logic to show an invariant holds or using induction?

I want to know if given a while loop: x = 0 while(x < 5){ x = x + 1 } I want to show that x (at the a ith iteration of the loop), the value of i is ...
33 views

### Where to get proofs of open problems checked? [closed]

I have found what I believe is a proof of related to an open problem in computer science. I've written it up in LaTeX, and I am looking for a way to get it evaluated. I know that cs.se/cstheory.se ...
29 views

### Linearithmic solution to finding closest pairs in an array of N elements

I am reading Algorithms 4ed by Sedgewick and Wayne. I came across this algorithm design question that asks the following: Write a program that given an array of N integers, finds a closest pair: two ...