fmrisc.ProgramExplorer.Judgements

Class Terminates

java.lang.Object

fmrisc.ProgramExplorer.Judgements.Terminates

public final class Terminates
extends java.lang.Object

The judgement "se, Is, VS |- C |v J F"

Constructor Summary

Constructors

Constructor and Description
Terminates(ParamSymbol method, StateType stype, TaskFolder tasks, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Create a termination judgement processor.

Method Summary

Modifier and Type	Method and Description
Formula	derive(Statement C, ValueSymbol[] J, Formula F) Apply the judgement se, Is, Vs |- C |v J F to prove that command C terminates when executed in a state in which F[J] holds where J is a vector of free variables in F that denotes the measure of the recursive methods in Is that may be called in C (J may be null which indicates that the current method is not recursive).

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

Terminates

public Terminates(ParamSymbol method,
                  StateType stype,
                  TaskFolder tasks,
                  java.util.Vector<TheorySymbol> theories,
                  Declaration[][] decls,
                  ErrorStream out)

Create a termination judgement processor.

Parameters:

method - the method in which the judged commands arise.

stype - the type of the state for the context of a command.

tasks - the folder to which to add termination-related tasks.

theories - the referenced theories (first is base theory)

decls - a sequence of declaration lists.

out - the stream to which to write error messages.

Method Detail

derive

public Formula derive(Statement C,
                      ValueSymbol[] J,
                      Formula F)

Apply the judgement se, Is, Vs |- C |v J F to prove that command C terminates when executed in a state in which F[J] holds where J is a vector of free variables in F that denotes the measure of the recursive methods in Is that may be called in C (J may be null which indicates that the current method is not recursive). Must be called only after C has been annotated with its judgement. As a side effect, generate the verification conditions to be proved and extend the judgement of C by a condition T on a state that is sufficient to ensure that the execution of C in that state terminates (excluding the termination of recursive function calls). T may be null which indicates TRUE (C terminates on every state). Returns the condition T. See Section 4.10 of "A Program Calculus", Is is set in the method, while se and Vs are not needed because identifiers have already been resolved to symbols.

Parameters:

C - the command C

J - the variable vector representing the termination measure

F - the condition on the state in which C is called

Returns:

the condition T (possibly null which indicates TRUE).