The tag has no wiki summary.

learn more… | top users | synonyms

0
votes
1answer
52 views

Finding a Hoare logic correctness proof for a Repeat-Until loop

How can we prove a program in repeat until using Hoare Logic? I've found a rule like this: {P} S {R}, {R ^ ~B -> P}, {R ^ B -> Q} for ...
0
votes
1answer
19 views

Hoare logic - partial/total correctnes and strength invariant

I'm studying Hoare logic and I can't understand the relation between partial and total correctness regarding loop invariant. Suppose for example that I have the following program: ...
1
vote
1answer
64 views

Encoding the pigeonhole principle in CBMC

CBMC is a Bounded Model Checker for ANSI-C and C++ programs. It also supports SystemC using Scoot. It allows verifying array bounds (buffer overflows), pointer safety, ex­cep­tions and ...
0
votes
1answer
105 views

applying CTL/LTL model-checking on some system

I apologies if my title is vague, I'm trying to apply CTL/LTL model-checking on some system written in java, however, I still don't understand how to reach a result using either of the approaches ...
10
votes
4answers
597 views

How do you check if two algorithms return the same result for any input?

How do you check if two algorithms (say, Merge sort and Naïve sort) return the same result for any input, when the set of all inputs is infinite? Update: Thank you Ben for describing how this is ...
4
votes
3answers
378 views

Hoare triple for assignment P{x/E} x:=E {P}

I am trying to understand Hoare logic presented at Wikipedia, Hoare logic at Wikipedia Apparently, if I understand correctly, a Hoare triple $$\{P\}~ C ~\{Q\}$$ means if P just before C, then Q ...