1 of 34

CS 5/6110, Software Correctness Analysis, Spring 2023

Ganesh Gopalakrishnan

School of Computing

University of Utah

Salt Lake City, UT 84112

2 of 34

History, Motivations

​

  • Historically the first verification approach considered
  • Recently TimSort was found to be buggy and upgraded
    • See Wikipedia article on the TimSort bug
    • Proved by people using the theorem prover called Key
  • A good intuition about how Hoare Logic verifiers work is important
  • Will study a Lisp-based verifier in Gordon’s book meanwhile

3 of 34

Good overviews of Hoare Logic

4 of 34

Let’s analyze an XOR-based swap

  • Basically a trick to swap two variables without a temp
  • Each following slide builds on the previous

5 of 34

6 of 34

7 of 34

8 of 34

9 of 34

10 of 34

11 of 34

12 of 34

13 of 34

14 of 34

15 of 34

16 of 34

17 of 34

Gordon’s example 20 (in Gordon’s book)

Here is an

“annotated

Program”

​

The question is

​

Does the

“ensures”

Clause hold?

18 of 34

Gordon’s example done by hand

19 of 34

Gordon’s g20 example and its “LI walk-back”

S = x*y at the output

20 of 34

In a Hoare-logic proving approach, one annotates the program

at the “loop head” with a LOOP INVARIANT

​

It must be true whenever the execution reaches that point

​

What is it?

21 of 34

In a Hoare-logic proving approach, one annotates the program

at the “loop head” with a LOOP INVARIANT

​

It must be true whenever the execution reaches that point

What is it?

The “remaining work” is X.

Thus, S + X*y = x*y

OR S = y * (x – X)

Then upon exit, S = y * x

22 of 34

23 of 34

24 of 34

With nested loops, we need more annotations

Here is an “optimized” version

of the same program

​

Method g20(x,y : nat) returns (S:nat)

Requires x > 0

Requires y > 0

Ensures S == x * y

{ var X,Y;

X := x; Y := y; S := 0;

​

while(X != 0)

​

{ while (X % 2 == 0)

​

{ Y := Y + Y ; X := X / 2; }

S := S+Y;

X := X-1;

}

}

25 of 34

With nested loops, we need more annotations

Here is an “optimized” version

of the same program

​

Method g20(x,y : nat) returns (S:nat)

Requires x > 0

Requires y > 0

Ensures S == x * y

{ var X,Y;

X := x; Y := y; S := 0;

​

while(X != 0) [ Loop Invariant Here ? ]

​

{ while (X % 2 == 0)

​

{ Y := Y + Y ; X := X / 2; }

S := S+Y;

X := X-1;

}

}

26 of 34

With nested loops, we need more annotations

Here is an “optimized” version

of the same program

​

Method g20(x,y : nat) returns (S:nat)

Requires x > 0

Requires y > 0

Ensures S == x * y

{ var X,Y;

X := x; Y := y; S := 0;

​

while(X != 0) [ Loop Invariant Here ? ]

[ Remaining “work” is still measured by X ]

[ If you pretend to do that much more, and add to S,

it should match our goal ]

{ while (X % 2 == 0)

{ Y := Y + Y ; X := X / 2; }

S := S+Y;

X := X-1;

}

}

27 of 34

With nested loops, we need more annotations

Here is an “optimized” version

of the same program

​

Method g20(x,y : nat) returns (S:nat)

Requires x > 0

Requires y > 0

Ensures S == x * y

{ var X,Y;

X := x; Y := y; S := 0;

​

while(X != 0) [ Loop Invariant Here ? ]

​

{ while (X % 2 == 0)

​

{ Y := Y + Y ; X := X / 2; }

S := S+Y;

X := X-1;

}

}

28 of 34

With nested loops, we need more annotations

Here is an “optimized” version

of the same program

​

The inner loop does “doubling”

of Y each time X is even

​

The well-founded relation

(to argue termination) is also

given

in one version of Dafny, it failed with 2Y…

have correspondence with author (Rustan)

Don't know if gone now

29 of 34

With nested loops, we need more annotations

Let’s at least get some experience

applying the WP rules

by hand

in one version of Dafny, it failed with 2Y…

have correspondence with author (Rustan)

Don't know if gone now

30 of 34

Gordon’s Prover with “proof generation” added by Mantha

31 of 34

Gordon’s Prover with “proof generation” added by Mantha

32 of 34

Gordon’s Prover with “proof generation” added by Mantha

33 of 34

Gordon’s Prover with “proof generation” added by Mantha

34 of 34

Gordon’s Prover with “proof generation” added by Mantha

Run using sbcl