LogicChecking

java.lang.Object
- fmrisc.ProgramExplorer.Semantics.LogicChecking

public final class LogicChecking
extends java.lang.Object

Type-check a logical theory.

Method Summary

All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type	Method and Description
`static LogicChecking`	`createChecker(ClassSymbol csymbol, Environment penv, ErrorStream error)` Create checker for processing logical entities in environment set up by the (already processed) local theory of a class.
`static LogicChecking`	`createChecker(ErrorStream error)` Create checker for processing logical entities in empty environment.
`LogicEnvironment`	`getLogicEnvironment()` Get the environment for looking up logic symbols.
`TCCGenerator`	`getTCCGenerator()` Get the generator for producing type checking conditions
`boolean`	`hasIntType(Term term, Type type, boolean gen)` Checks if term has type INT, may generate type checking condition.
`boolean`	`hasNatType(Term term, Type type, boolean gen)` Checks if term has type NAT, may generate type checking condition.
`static boolean`	`isBooleanType(Type type)` Check whether type denotes a boolean.
`static boolean`	`isIntegerType(Type type)` Determine whether type is (a subtype of) the integer type.
`boolean`	`process(Declaration[] decls)` Type-check declaration sequence in current theory.
`boolean`	`process(Formula formula)` Type-check formula in current theory.
`Type`	`process(Term term)` Type-check term in current theory and, as a side effect, annotate the term with the type.
`static boolean`	`process(TheorySymbol tsymbol, ErrorStream error)` Process the theory symbol i.e.
`Type`	`process(Type type)` Process type expression in current theory.
`boolean`	`processFormula(Formula formula)` Process formula and create type-checking conditions in context set up by setStateContext().
`boolean`	`processIntTerm(Term term)` Process term denoting an integer number and create type-checking conditions in context set up by setStateContext().
`Type`	`processTermCore(Term term)` Type-check term in current theory and, as a side effect, annotate the term with the type.
`void`	`resetStateContext()` Reset the program state context.
`void`	`setStateContext(Formula pre, StateType type, Name[] vars, Name[] excs, TaskFolder folder)` Set the current program state context.
`Type`	`subType(Type type0, Type type1)` Returns greatest lower bound of type0 and type1 (null, if none exists); does not generate tccs.
`static boolean`	`validDefinitionType(Type type)` decide whether definition type is first order, i.e., - a function type is only allowed at the top level - the type BOOLEAN is only allowed at the top level or as the range of the function type
`static boolean`	`validTermType(Type type)` decide whether type does not contain a function type or BOOLEAN.

Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

- Method Detail
  - process
```
public static boolean process(TheorySymbol tsymbol,
                              ErrorStream error)
```
    Process the theory symbol i.e. type-check the associated declaration and populate the content of the symbol with it.
    
    Parameters:
    
    tsymbol - the theory symbol with a non-empty declaration.
    
    error - the stream on which to write the error messages.
    
    Returns:
    
    true iff no problem occurred in type-checking.
  - createChecker
```
public static LogicChecking createChecker(ClassSymbol csymbol,
                                          Environment penv,
                                          ErrorStream error)
```
    Create checker for processing logical entities in environment set up by the (already processed) local theory of a class.
    
    Parameters:
    
    csymbol - the class symbol
    
    penv - the program environment used by the checker.
    
    error - the stream on which to write error messages.
    
    Returns:
    
    a checker for processing logical entities in theory environment.
  - createChecker
```
public static LogicChecking createChecker(ErrorStream error)
```
    Create checker for processing logical entities in empty environment.
    
    Parameters:
    
    error - the stream on which to write error messages.
    
    Returns:
    
    a checker for processing logical entities.
  - getLogicEnvironment
```
public LogicEnvironment getLogicEnvironment()
```
    Get the environment for looking up logic symbols.
    
    Returns:
    
    the environment.
  - getTCCGenerator
```
public TCCGenerator getTCCGenerator()
```
    Get the generator for producing type checking conditions
    
    Returns:
    
    the type checking condition generator
  - setStateContext
```
public void setStateContext(Formula pre,
                            StateType type,
                            Name[] vars,
                            Name[] excs,
                            TaskFolder folder)
```
    Set the current program state context.
    
    Parameters:
    
    pre - the precondition of the method (may be null).
    
    type - the current state type (may be null).
    
    vars - the variable frame of the current program state (may be null).
    
    excs - the exceptions of the current program state (may be null).
    
    folder - the folder for generating type checking conditions
  - resetStateContext
```
public void resetStateContext()
```
    Reset the program state context.
  - validDefinitionType
```
public static boolean validDefinitionType(Type type)
```
    decide whether definition type is first order, i.e., - a function type is only allowed at the top level - the type BOOLEAN is only allowed at the top level or as the range of the function type
    
    Parameters:
    
    type - an already processed type arising from a type definition
    
    Returns:
    
    true iff the type is first order
  - validTermType
```
public static boolean validTermType(Type type)
```
    decide whether type does not contain a function type or BOOLEAN.
    
    Parameters:
    
    type - an already processed type
    
    Returns:
    
    true iff the type does not contain a function type or type BOOLEAN
  - processFormula
```
public boolean processFormula(Formula formula)
```
    Process formula and create type-checking conditions in context set up by setStateContext().
    
    Parameters:
    
    formula - the formula to be processed.
    
    Returns:
    
    true, if everything went fine, false otherwise.
  - processIntTerm
```
public boolean processIntTerm(Term term)
```
    Process term denoting an integer number and create type-checking conditions in context set up by setStateContext().
    
    Parameters:
    
    term - the term to be processed.
    
    Returns:
    
    true, if everything went fine, false otherwise.
  - process
```
public boolean process(Declaration[] decls)
```
    Type-check declaration sequence in current theory.
    
    Parameters:
    
    decls - the declarations to be type-checked.
    
    Returns:
    
    true iff everything went okay.
  - process
```
public boolean process(Formula formula)
```
    Type-check formula in current theory.
    
    Parameters:
    
    formula - the formula to be type-checked.
    
    Returns:
    
    true if everything went fine, false otherwise
  - process
```
public Type process(Term term)
```
    Type-check term in current theory and, as a side effect, annotate the term with the type.
    
    Parameters:
    
    term - the term to be type-checked.
    
    Returns:
    
    the resulting type (null, if an error occurred)
  - processTermCore
```
public Type processTermCore(Term term)
```
    Type-check term in current theory and, as a side effect, annotate the term with the type.
    
    Parameters:
    
    term - the term to be type-checked.
    
    Returns:
    
    the resulting type (null, if an error occurred)
  - process
```
public Type process(Type type)
```
    Process type expression in current theory.
    
    Parameters:
    
    type - the type expression to be type-checked.
    
    Returns:
    
    the resulting canonical type (null, if an error occurred)
  - hasNatType
```
public boolean hasNatType(Term term,
                          Type type,
                          boolean gen)
```
    Checks if term has type NAT, may generate type checking condition.
    
    Parameters:
    
    term - the term (may be null, if gen is false).
    
    type - its type determined by the type checker.
    
    gen - true if type checking condition may be generated.
    
    Returns:
    
    true iff term has type NAT.
  - hasIntType
```
public boolean hasIntType(Term term,
                          Type type,
                          boolean gen)
```
    Checks if term has type INT, may generate type checking condition.
    
    Parameters:
    
    term - the term (may be null, if gen is false).
    
    type - its type determined by the type checker.
    
    gen - true if type checking condition may be generated.
    
    Returns:
    
    true iff term has type INT.
  - subType
```
public Type subType(Type type0,
                    Type type1)
```
    Returns greatest lower bound of type0 and type1 (null, if none exists); does not generate tccs.
    
    Parameters:
    
    type0 - a type
    
    type1 - a type
    
    Returns:
    
    the greatest lower bound of type0 and type1 (null, if none exists)
  - isIntegerType
```
public static boolean isIntegerType(Type type)
```
    Determine whether type is (a subtype of) the integer type.
    
    Parameters:
    
    type - the type.
    
    Returns:
    
    true if the type is an integer type.
  - isBooleanType
```
public static boolean isBooleanType(Type type)
```
    Check whether type denotes a boolean.
    
    Parameters:
    
    type - the type.
    
    Returns:
    
    true if the type denotes a boolean.

Class LogicChecking

Method Summary

Methods inherited from class java.lang.Object

Method Detail

process

createChecker

createChecker

getLogicEnvironment

getTCCGenerator

setStateContext

resetStateContext

validDefinitionType

validTermType

processFormula

processIntTerm

process

process

process

processTermCore

process

hasNatType

hasIntType

subType

isIntegerType

isBooleanType