wyil.util.type

Class ExplicitCoercionOperator

java.lang.Object

wyil.util.type.SubtypeOperator

wyil.util.type.ExplicitCoercionOperator

public class ExplicitCoercionOperator
extends SubtypeOperator

The explicit coercion operator extends the implicit coercion operator to include coercions which must be specified with an explicit cast operation. This is necessary because such coercions correspond to a loss of precision and, hence, may fail at runtime. An example is the following

 char f(int x):
     return (char) x
 

The above will only compile if the explicit (char) cast is provided. This is required because a char corresponds only to a subset of the possible integers (i.e. those codepoints defined by the Unicode standard). The semantics of the Whiley language dictate that, should the integer lie outside the range of permissible code points, then a runtime fault is raised.

NOTE: as for the subtype operator, both types must have been normalised beforehand to guarantee correct results from this operator.

Author:

David J. Pearce

Field Summary

Fields inherited from class wyil.util.type.SubtypeOperator

from, to

Constructor Summary

Constructors

Constructor and Description
ExplicitCoercionOperator(Automaton fromAutomata, Automaton toAutomata, LifetimeRelation lr)

Method Summary

Modifier and Type	Method and Description
protected boolean	intersectRecords(int fromIndex, boolean fromSign, int toIndex, boolean toSign) Check for intersection between two states with kind K_RECORD.
boolean	isIntersectionInner(int fromIndex, boolean fromSign, int toIndex, boolean toSign)

Methods inherited from class wyil.util.type.SubtypeOperator

isIntersection, isSubtype, isSupertype

Methods inherited from class java.lang.Object

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

Constructor Detail

ExplicitCoercionOperator

public ExplicitCoercionOperator(Automaton fromAutomata,
                                Automaton toAutomata,
                                LifetimeRelation lr)

Method Detail

isIntersectionInner

public boolean isIntersectionInner(int fromIndex,
                                   boolean fromSign,
                                   int toIndex,
                                   boolean toSign)

Overrides:

isIntersectionInner in class SubtypeOperator

intersectRecords

protected boolean intersectRecords(int fromIndex,
                                   boolean fromSign,
                                   int toIndex,
                                   boolean toSign)

Check for intersection between two states with kind K_RECORD. The distinction between open and closed records adds complexity here.

Intersection between closed records is the easiest case. The main examples are:

• {T1 f, T2 g} & {T3 f, T4 g} = if T1&T3 and T2&T4.
• {T1 f, T2 g} & {T3 f, T4 h} = false.
• {T1 f, T2 g} & !{T3 f, T4 g} = if T1&!T3 or T2&!T4.
• {T1 f, T2 g} & !{T3 f} = false.
• !{T1 f} & !{T2 f} = true.

Intersection between a closed and open record is similar. The main examples are:

• {T1 f, T2 g, ...} & {T3 f, T4 g} = if T1&T3 and T2&T4.
• {T1 f, ...} & {T2 f, T3 g} = if T1&T2.
• {T1 f, T2 g, ...} & {T3 f, T4 h} = false.
• {T1 f, T2 g, ...} & !{T3 f, T4 g} = if T1&!T3 or T2&!T4.
*
• !{T1 f, T2 g, ...} & {T3 f, T4 g} = if T1&!T3 or T2&!T4.
*
• {T1 f, ...} & !{T2 f, T3 g} = true.
• {T1 f, T2 g, ...} & !{T3 f, T4 h} = false.
• !{T1 f,...} & !{T2 f} = true.

Overrides:

intersectRecords in class SubtypeOperator

Parameters:

fromIndex - --- index of from state

fromSign - --- sign of from state (true = normal, false = inverted).

toIndex - --- index of to state

toSign - --- sign of from state (true = normal, false = inverted).

Returns:

--- true if such an intersection exists, false otherwise.