The notion of symbolic output tape is discrete, because the elements are in the execution order and the time history has been saved in the indexes of the tape. Pnueli (1977) has suggested that temporal logic, a variant of modal logic, could be suitable for specifying properties of reactive and concurrent systems, which is a larger scope than the tape formalism, but by adding several tapes it is possible to model a system, which has a set of infinite sequences of states and executions. The specification language Pnueli presented for this purpose is linear temporal logic (Emerson, 1990). We have extended their logic further.

Building a resolution tree: theorems, operands and constraints

The following framework to define PC hypotheses for learning code and validating programs is downwards compatible with temporal logic having similar functionalities.  Typical hypotheses are either assumptions or specifications describing the relevant program flow with its side effects. These contain, in the time order, critical elements like the main method in the beginning and some problematic element as targets of the program flow.

The main elements of the framework are:

  • An operand, which means an explicit pointer to the ouput tape possibly including several tape references.
  • A constraint, the purpose of which is to signal about logical conflicts.
  • A theorem, which is a small logical task for the tool to be proved according to the contents of the tape.

For a proof, constraints are needed for validating the operand references. However, even a single operand can be a theorem, because a tape is valid only if the specified operand can be found in the tape, which rule implements an existence theorem.

Specifying_Constraints

Any operand of the constraints can be defined to be inside a class, an object, a method or inside a loop. If there is the selected operand in the specified place then true is returned (causing no contradiction). The other type of constraint is relative. An operand can have a relation before, after or between related to some other operands. Otherwise, false is returned.

The most typical constraint in verifying a computation in the tape is its location. The others are causality and precedence rules. There are the following alternatives to express a location constraint:

  • Global: The operands can be anywhere in the tape.
  • Inside method: Operands separated between the start and end elements of a method.
  • Inside object: Operands separated transitively from the method to the corresponding object (having a correspondence in the Java object and a specific Java class).
  • Inside class: Operands separated transitively from the method to the corresponding object (having a correspondency in the Java object and a specific Java class).
  • Inside loop: Operands separated in a loop between its start and end elements.
  • A place in the tape can be expressed by the definitions before, after and between.
  • An explicit place in the tape can be defined by an atom reference.
  • Sometimes any place is accepted.
Advertisements