Proposal : Object Propositions

predicates can be used to express properties of elds using integers, but reasoning about integers is di cult. We are going to employ a theorem prover to prove properties about integers. Most probably, we are going to use the Z3 theorem prover [3]. Kevin Bierho has implemented a tool called JavaSyp [1] that uses the SMT solver Z3 to formally verify Java code. We initially wanted to modify JavaSyp in order to implement Oprop, but that proved to be a di cult task. There are many details that are di erent between JavaSyp and what Oprop needs to do: JavaSyp uses borrowing and capture/release because the tool does not implement fractional permissions. Oprop does not use borrowing, but instead it uses fractional permissions. Fractions give more precision than the borrowing mechanism and we are going to implement fractional permissions. Oprop will implement the pack/unpack mechanism, while JavaSyp does not implement this mechanism. JavaSyp implements instead exposure blocks" that show how elds should be accessed. These features are closely related: when the elds of an object are unpacked (when the object proposition that encapsulated them is unpacked), we can think of them as being exposed". In Bierho 's system, there are unique" and immutable" exposure blocks. Fields can be assigned inside unique exposure blocks, with eld reads yielding the eld's original permission. Inside an immutable block, reading elds results in a weakened eld permission. The technical di erence is that in my system I do not have immutable permissions, but instead one can always write to the elds of an object (in some cases, one has to make sure that the invariant is preserved). I acknowledge that this is just an incidental di erence and the ideas of pack/unpack vs. exposure blocks are very similar. JavaSyp has class invariants, but Oprop will not have them and instead it will have invariants for objects that are shared. Our plan is to create a tool similar to JavaSyp that rst translates the code and speci cations into an intermediary language (such as those used by Dafny or Chalice, from the RiSE group at Microsoft Research [7]) and then use that intermediary tool together with Z3 to obtain the nal result. 9 Validation and Evaluation We will evaluate the usefulness of the Oprop tool and of the object proposition methodology by designing a user study where we observe how the Oprop plugin improves the e ciency of programmers. We will also try to solve the open problem Finalizers, that will be described below, using our methodology. We have already made some contributions to the speci cation and veri cation of the Composite pattern, and we will nalize the veri cation of the Composite pattern.