Architecture

4 Architecture

4.1 Basics

4.1.1 Model files

A proof is made inside a section called JackProof where the hypothesis are written as variable and the goal to prove is a lemma. All the definitions are in the library which can be divided into 2 parts, the static part and the dynamic one. The static part correspond to the files littleHelper1 and littleHelper2. The first contains all the axiom and lemmas concerning basic arithmetic. The second contains some definitions on overriding different type of variables, messing with references and with instances. The dynamic part contains mainly things dealing with the definition of classes and subtypes, and some other that couldn't be generated statically.

4.1.2 A bit on the memory model

In the Coq Plugin we map the primitive Java types (int, short, long, byte, char, - float and double are not supported by Jack) directly to the type Z in Coq. This is useful in that we can use the arithmetic tactics already present in Coq (namely omega and ring) to solve the proof obligations containing arithmetic. Anyway we have had to add some lemmas to guarantee the range of these naturals (sometimes Jack explicitly writes the domain of a variable in a proof obligation). There are also arithmetic conversion functions when for instance long are converted to short, etc... These datatypes are defined in the file littleHelper1.v.

Apart from the numbers; all the other types in Java are of the type class or of the type array. These two types are in Java some kind of reference to an object in the memory. In Coq they are all of type REFERENCES. Objects of type REFERENCES have special properties. If they have already been initialized (they are used outside of their constructor); they equals null or are an instance. An instance of an object cannot be null; but within its constructor an object can be not null and not an instance. Java being an object oriented language, each class is a subtype of another, it is represented in Coq with the inductive construct subtypes.

In the references there are some special cases the arrays and the String. They are special because they are at the same time some primitive types and some classes.

Summary:

Construction	Type	Java Correspondance
t_int	Set	int
t_short	Set	short
t_long	Set	long
t_byte	Set	byte
t_char	Set	char
class c_Class	Classes -> Types	Class
array (class c_Class) 1	Types -> Z -> Types	Class []
null	REFERENCES	null
subtypes	Types -> Types -> Prop	-
instances	REFERENCES -> Prop	-
typeof	REFERENCES -> Types	-

Jack also manages variable aliasing. In Coq this is done using the functions overridingCoupleZ in the case of a number (since every number is mapped to Z), overridingCoupleRef in the case of a reference (a class), and overridingArray in the case of an array. This functions are of the following form:

overridingCouple f obj inst res :=

if (= obj inst) then

res

else

f (obj).

4.2 Tactics (Quick Description)

The proof obligations generated by Jack have often the same forms or the same subgoals: we have to check the length of some array (it has to be positive!) we have to check the range of a dereferencing; that a class is really a subtype of another, a variable is not null and is an instance... These proofs are repetitive and most of the time easy to solve (it takes less then 10 lines). So we decided to use Ltac in order to solve these subgoals.

We have made two kind of tactics, those which are general and works more on a syntactic side, and those which are given by the specific model and are more Jack specific. In the first kind we have elimAnd to eliminate most of the and generated by Jack in the hypothesis: if an hypothesis has the form H: a -> b it is divided in H1: a, H2: b, the other case is when an hypothesis has the form H: a -> b /\ c it will be replaced by H1: a -> b, H2: a -> c. This tactic has been really useful, because Jack is used to add all the invariant of a same class into one big hypothesis, each invariant jointed by an and, so if we want to use one of the invariant we are forced to break up the and. The same behaviour can be seen if we have a specification in a JML's require made of and which happens often.

Another general tactic is the one called tryApply which tries to apply to the current goal every single hypothesis. It is useful when you have many hypothesis and you can't really dig into, or when you try to do proofs in a more automatic fashion. Most of these general tactics are already built-ins in Coq interactive prover, notably within intuition or eapply, the only problem is that the Coq's built-in tactics take often too much resources when there is a lot of hypothesis in the goal you try to solve; and this situation comes often in Jack; so we have had to develop more precise tactics in order to keep the complexity of each action low.

The more specific tactics are for instance arrtac which help solve goals about arrays. arrtac is really powerful when trying to solve a goal of the form instances var where var is an array, or of the form 0 <= arraylength var. It instanciate the right axioms (namely ArrayTypeAx and/or arraylenAx) and generate some subgoals on the types of the target array.

The other really-specific-to-Jack tactic is solveOver. It aims to simplify formulas containing the overridingCouple constructs. when unfolded the function overridingCouple is an if construction which can be easily broken in generating the different cases, i.e. adding as an hypothesis the condition is false or the condition is true and by forcing to solve the goal with each different condition.

4.3 Library

Coq plugin's library is made of two sections:

The local tactics, with some documentation here.
The library defining the different constructions used in proof obligations which have this documentation.