Pekeraliasing i Hoare-logikk

Abstract

We study problems that comes up when Hoare logic is used to prove programs written in object oriented languages (i.e. Java). The main problem we study, is due to pointer aliasing. Traditional Hoare logic handles programs where every syntactical distinct variable name represent a distinct storage location. Two variables x and y will always represent distinct locations. This does not hold when we extend our programming language width objects and pointers to objects. If two pointer variables x and y points to the same object, then (with dot notation) x.a and y.a represent the same location. This lead us into the unfortunate situation where it is not straight forward to prove the simple Hoare triplet {x.a=4}y.a:=y.a+1{x.a=5}. The assignment modifies the condition to seemingly unrelated objects.

In our example study, we look into various proofs for a linked list data structure. After trying and failing, we come up with methods to prove programs both backward and forward. The method for backward construction is similar to a method developed by R. Bornat, but we use a simpler sematic. It is important to be careful when we compare references. If x and y points to the same object, and we do an assignment to x.a, we also have to update y.a. The hard part is to decide if two arbitrary references refers to the same object.

We also compare the two methods we got for proof construction (i.e forward and backward). We find several advantages with forward reasonning. If the precondition to an assignment contains a lot of alias information, this information can be used "as we go" in forward reasonning. In backward proof construction, we might have to go all the way back to the precondition before we can use this information. The same goes for information we get from test. In many cases, this leads us to simpler proof in the forward case. The predicates are simpler. We also see an advantage in the expressive power of the predicates in the forward case. In forward reasonning, the predicates always contains all the alias information we can have at a given point in the proof. This is not the case in backward construction.