Primitive Predicate Extension. Here we explain the primitive predicate extension with an example. If we wish in this example to verify a change of program structure during weaving, we know that a new primitive predicate that represents inheritance relations be- tween a class and its super class is needed. We try to add a primitive predicate called extends(Subclass, Superclass) that becomes true when Subclass ex- tends Superclass regardless of direct or indirect inheri- tance. First, we implement a rule for mapping some parts of the program analysis result needed for verifying the inheri- tance relation to the Prolog facts. The mapping rule is im- plemented as the method named toFacts in Figure 4. We implement this method to return the Prolog facts that corre- spond to the parts of the program analysis result that repre- sent the inheritance relation. For instance, since the analysis result contains direct inheritance relations, we implement the method to map each relation to the Prolog fact named directExtends. For instance, when the program anal- ysis result contains the inheritance relation that A class di- rectly extends the B class, the method returns the following fact: directExtends(’A’, ’B’). Next, we define a rule for verifying the extends primitive predicate. This definition is implemented as the toRule factory method that returns a Prolog rule. For instance, to verify the extends predicate, we implement the method to return the following rule: extends(Subclass, Superclass) :- directExtends(Subclass, Superclass). extends(Subclass, Superclass) :- directExtends(Subclass0, Superclass), extends(Subclass, Subclass0). Although the rule and the facts are shown in Prolog, the contract verifier provides a method for describing these as Java class objects. We can extend the primitive predicate set of the verifier only by implementing a simple factory class. This extensibility is useful for approaches that attempt to verify the correctness of weaving.
