Module Contract.Names

Exported Functions

isSpecName :: String -> Bool   

Is this the name of a specification?

toSpecName :: String -> String   

Transform a name into a name of the corresponding specification by adding the suffix "'spec".

toSpecQName :: (String, String) -> (String, String)   

Transform a qualified name into a name of the corresponding specification by adding the suffix "'spec".

fromSpecName :: String -> String   

Drop the specification suffix "'spec" from the name:

isPreCondName :: String -> Bool   

Is this the name of a precondition?

toPreCondName :: String -> String   

Transform a name into a name of the corresponding precondition by adding the suffix "'pre".

toPreCondQName :: (String, String) -> (String, String)   

Transform a qualified name into a name of the corresponding precondition by adding the suffix "'pre".

fromPreCondName :: String -> String   

Drop the precondition suffix "'pre" from the name:

isPostCondName :: String -> Bool   

Is this the name of a precondition?

toPostCondName :: String -> String   

Transform a name into a name of the corresponding prostcondition by adding the suffix "'post".

toPostCondQName :: (String, String) -> (String, String)   

Transform a qualified name into a name of the corresponding postcondition by adding the suffix "'post".

fromPostCondName :: String -> String   

Drop the postcondition suffix "'post" from the name:

isNonFailName :: String -> Bool   

Is this the name of a precondition?

toNonFailName :: String -> String   

Transform a name into a name of the corresponding prostcondition by adding the suffix "'post".

toNonFailQName :: (String, String) -> (String, String)   

Transform a qualified name into a name of the corresponding postcondition by adding the suffix "'post".

fromNonFailName :: String -> String   

Drop the postcondition suffix "'nonfail" from the name:

decodeContractQName :: (String, String) -> (String, String)   

Transforms a qualified operation name starting with op_xh1...hn', where each hi is a two digit hexadecimal number, into the name of corresponding to the ord values of h1...hn. For instance, op_x263E'nonfail is transformed into &>'nonfail.

decodeContractName :: String -> String   

Transforms an operation name starting with op_xh1...hn', where each hi is a two digit hexadecimal number, into the name of corresponding to the ord values of h1...hn. For instance, op_x263E'nonfail is transformed into &>'nonfail.

encodeContractQName :: (String, String) -> (String, String)   

Transforms a qualified operation name of the form fn'tail into a valid identifier. Thus, if fn contains any non-alphanumeric characters, the name will be transformed into op_xh1...hn', where each hi is the two digit hexadecimal number corresponding to the i-th character of fn. For instance, &>'nonfail is transformed into op_x263E'nonfail.

encodeContractName :: String -> String   

Transforms an operation name of the form fn'tail into a valid identifier. Thus, if fn contains any non-alphanumeric characters, the name will be transformed into op_xh1...hn', where each hi is the two digit hexadecimal number corresponding to the i-th character of fn. For instance, &>'nonfail is transformed into op_x263E'nonfail.