Checking

java.lang.Object
- fmrisc.ProofNavigator.Semantics.Checking

public final class Checking
extends java.lang.Object

type checking routines

Constructor Summary

Constructors
Constructor and Description

Checking()

Constructors
Constructor and Description
`Checking()`

Method Summary

All Methods Static Methods Concrete Methods
Modifier and Type	Method and Description
`static Type`	`canonical(Type type)` Returns canonical version of type (equality of two types implies the equality of the canonical version of the types).
`static Type`	`canonicalTcc(Type type)` Returns canonical version of type (equality of two types implies the equality of the canonical version of the types).
`static TypeExpression`	`clearSubtypes(Type type, Expression exp)` return version of type where subtypes and subranges (including NAT) are replaced by their base types; the corresponding constraints are returned as a formula which a corresponding expression exp has to fulfill
`static AtomicType`	`getBitType()` Get canonical type BIT
`static AtomicType`	`getBooleanType()` Get canonical type BOOLEAN
`static AtomicType`	`getIntType()` Get canonical type INT
`static AtomicType`	`getNatType()` Get canonical type NAT
`static AtomicType`	`getRealType()` Get canonical type REAL
`static java.util.Collection<Symbol>`	`getReferencedSymbols()` get collection of referenced symbols
`static boolean`	`hasType(Expression exp, Type etype, Type type, boolean tcc)` returns true iff expr of type etype matches type.
`static void`	`init()` Initialize checking state
`static boolean`	`isBoolean(Type type)` checks if type equals BOOLEAN
`static boolean`	`isInt(Type type)` checks if type equals INT
`static boolean`	`isNat(Type type)` checks if type equals NAT
`static boolean`	`isReal(Type type)` checks if type equals REAL
`static Type`	`processDefinitionTerm(Expression value)` type check definition term with potential first-order type check
`static Type`	`processFormula(Expression value)` type check value without first-order type check
`static Type`	`processTerm(Expression value)` type check term with potential first-order type check
`static Type`	`processTermOrFormula(Expression value)` type check term with potential first-order type check
`static void`	`resetReferencedSymbols()` reset collection of referenced symbols
`static void`	`setStrongerTypes(boolean stronger)` signals whether stronger type discipline is to be preserved
`static void`	`setWeakerTypes(boolean weaker)` signals whether weaker type discipline is to be preserved
`static void`	`simplifyNames(TypedIdentifier[] vars, Environment env, Expression exp)` Simplify names of local variables to their base names if no name capture can occur.
`static Type`	`subType(Type type0, Type type1)` return greatest subtype 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`	`validTerm(Expression exp)` decide whether expression denotes a term
`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

- Constructor Detail
  - Checking
```
public Checking()
```
- Method Detail
  - init
```
public static void init()
```
    Initialize checking state
  - setStrongerTypes
```
public static void setStrongerTypes(boolean stronger)
```
    signals whether stronger type discipline is to be preserved
    
    Parameters:
    
    stronger - is true iff stronger type discipline is to be preserved
  - setWeakerTypes
```
public static void setWeakerTypes(boolean weaker)
```
    signals whether weaker type discipline is to be preserved
    
    Parameters:
    
    weaker - is true iff weaker type discipline is to be preserved
  - getBooleanType
```
public static AtomicType getBooleanType()
```
    Get canonical type BOOLEAN
    
    Returns:
    
    the type.
  - getBitType
```
public static AtomicType getBitType()
```
    Get canonical type BIT
    
    Returns:
    
    the type.
  - getIntType
```
public static AtomicType getIntType()
```
    Get canonical type INT
    
    Returns:
    
    the type.
  - getNatType
```
public static AtomicType getNatType()
```
    Get canonical type NAT
    
    Returns:
    
    the type.
  - getRealType
```
public static AtomicType getRealType()
```
    Get canonical type REAL
    
    Returns:
    
    the type.
  - isBoolean
```
public static boolean isBoolean(Type type)
```
    checks if type equals BOOLEAN
    
    Parameters:
    
    type - the type.
    
    Returns:
    
    true iff type equals BOOLEAN
  - isInt
```
public static boolean isInt(Type type)
```
    checks if type equals INT
    
    Parameters:
    
    type - the type.
    
    Returns:
    
    true iff type equals INT
  - isNat
```
public static boolean isNat(Type type)
```
    checks if type equals NAT
    
    Parameters:
    
    type - the type.
    
    Returns:
    
    true iff type equals NAT
  - isReal
```
public static boolean isReal(Type type)
```
    checks if type equals REAL
    
    Parameters:
    
    type - the type.
    
    Returns:
    
    true iff type equals REAL
  - getReferencedSymbols
```
public static java.util.Collection<Symbol> getReferencedSymbols()
```
    get collection of referenced symbols
    
    Returns:
    
    the collection.
  - resetReferencedSymbols
```
public static void resetReferencedSymbols()
```
    reset collection of referenced symbols
  - canonical
```
public static Type canonical(Type type)
```
    Returns canonical version of type (equality of two types implies the equality of the canonical version of the types). No type-checking conditions are generated.
    
    Parameters:
    
    type - the type
    
    Returns:
    
    the canonical version of the type (null, if an error occured)
  - canonicalTcc
```
public static Type canonicalTcc(Type type)
```
    Returns canonical version of type (equality of two types implies the equality of the canonical version of the types). Type-checking conditions may be generaed.
    
    Parameters:
    
    type - the type
    
    Returns:
    
    the canonical version of the type (null, if an error occured)
  - 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
  - validTerm
```
public static boolean validTerm(Expression exp)
```
    decide whether expression denotes a term
    
    Parameters:
    
    exp - the expression to be checked
    
    Returns:
    
    true iff the expression denotes a term
  - processDefinitionTerm
```
public static Type processDefinitionTerm(Expression value)
```
    type check definition term with potential first-order type check
    
    Parameters:
    
    value - the definition term to be type checked
    
    Returns:
    
    the type of the value or null if typechecking encountered error
  - processTerm
```
public static Type processTerm(Expression value)
```
    type check term with potential first-order type check
    
    Parameters:
    
    value - the term to be type checked
    
    Returns:
    
    the type of the term or null if typechecking encountered error
  - processFormula
```
public static Type processFormula(Expression value)
```
    type check value without first-order type check
    
    Parameters:
    
    value - the value to be type checked
    
    Returns:
    
    the type of the value or null if typechecking encountered error
  - processTermOrFormula
```
public static Type processTermOrFormula(Expression value)
```
    type check term with potential first-order type check
    
    Parameters:
    
    value - the term to be type checked
    
    Returns:
    
    the type of the term or null if typechecking encountered error
  - hasType
```
public static boolean hasType(Expression exp,
                              Type etype,
                              Type type,
                              boolean tcc)
```
    returns true iff expr of type etype matches type. may add as a side effect a type checking condition to the global context. the following general rules succeed without generating TCCs: exp: T matches T exp: SUBTYPE(p:T to BOOL) matches T the following general rule succeeds by generating a TCC: exp: T matches SUBTYPE(T) if p(exp) the following structural rules do not generate TCCs: exp: A to B matches A0 to B0, if A0 matches A and B matches B0 exp: ARRAY A OF B matches ARRAY A0 OF B0, if A0 matches A and B matches B0 the following structural rules *may* generate TCCs: exp: [T,...] matches [T0,...], if exp.0: T matches T0, ... exp: [#f:T,...#] matches [#f:T0,...], if exp.f: T matches T0, ... as for arithmetic, the relationship is as follows: [a..b] lt INT lt REAL NAT lt INT REAL0 lt REAL (REAL0, i.e. REAL without 0, is only internally used to denote the second argument type of the / operator and thus trigger a TCC) the corresponding conversions from left to right succeed without generating TCCs; conversions are applied transitively. as for the conversion from right to left, we have: exp: REAL matches INT if (EXISTS (x:INT): x=exp) // switched off because of CVCL problem exp: INT matches [a..b] if a leq exp and exp leq b exp: INT matches NAT if 0 leq exp exp: REAL matches REAL0 if exp /= 0 as for subranges of INT, we have exp: NAT matches [a..b] if (a leq 0 || a leq exp) and (exp leq b) exp: [a..b] matches NAT if 0 leq a || 0 leq exp exp: [a..b] matches [c..d] if (c leq a || c leq exp) and (b leq d || exp leq d) if rules are applied transitively, the conditions are appropriately conjoined, e.g. exp: REAL to SUBTYPE(p:[a..b] to BOOL) generates the TCC (EXISTS (x:INT): x=exp) and a leq exp and exp leq b and p(exp)
    
    Parameters:
    
    exp - the expression (may be null if tcc is false)
    
    etype - its type
    
    type - the type which expr:etype is expected to match
    
    tcc - true iff a tcc may be generated
    
    Returns:
    
    true iff the matching succeeds
  - subType
```
public static Type subType(Type type0,
                           Type type1)
```
    return greatest subtype of type0 and type1 (null, if none exists) does not generate tccs.
    
    Parameters:
    
    type0 - a type
    
    type1 - a type
    
    Returns:
    
    the subtype of type0 and type1 (or null, if none exists)
  - clearSubtypes
```
public static TypeExpression clearSubtypes(Type type,
                                           Expression exp)
```
    return version of type where subtypes and subranges (including NAT) are replaced by their base types; the corresponding constraints are returned as a formula which a corresponding expression exp has to fulfill
    
    Parameters:
    
    type - the type to be cleared
    
    exp - an expression of this type
    
    Returns:
    
    a pair of cleared type and formula (may be null if no condition generated) or null (if cleared type is identical to given type)
  - simplifyNames
```
public static void simplifyNames(TypedIdentifier[] vars,
                                 Environment env,
                                 Expression exp)
```
    Simplify names of local variables to their base names if no name capture can occur.
    
    Parameters:
    
    vars - local variables
    
    env - the environment in which the local variables are introduced.
    
    exp - the expression within which the variables are referenced.

Class Checking

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Constructor Detail

Checking

Method Detail

init

setStrongerTypes

setWeakerTypes

getBooleanType

getBitType

getIntType

getNatType

getRealType

isBoolean

isInt

isNat

isReal

getReferencedSymbols

resetReferencedSymbols

canonical

canonicalTcc

validDefinitionType

validTermType

validTerm

processDefinitionTerm

processTerm

processFormula

processTermOrFormula

hasType

subType

clearSubtypes

simplifyNames