Module Contract.Names

This module contains some operations to define and manipulate the names of contracts (i.e., specification and pre/postconditions) in a Curry program.

Author: Michael Hanus

Version: April 2019

Summary of exported operations:

isSpecName :: String -> Bool  Deterministic 
Is this the name of a specification?
toSpecName :: String -> String  Deterministic 
Transform a name into a name of the corresponding specification by adding the suffix "'spec".
toSpecQName :: (String,String) -> (String,String)  Deterministic 
Transform a qualified name into a name of the corresponding specification by adding the suffix "'spec".
fromSpecName :: String -> String  Deterministic 
Drop the specification suffix "'spec" from the name:
isPreCondName :: String -> Bool  Deterministic 
Is this the name of a precondition?
toPreCondName :: String -> String  Deterministic 
Transform a name into a name of the corresponding precondition by adding the suffix "'pre".
toPreCondQName :: (String,String) -> (String,String)  Deterministic 
Transform a qualified name into a name of the corresponding precondition by adding the suffix "'pre".
fromPreCondName :: String -> String  Deterministic 
Drop the precondition suffix "'pre" from the name:
isPostCondName :: String -> Bool  Deterministic 
Is this the name of a precondition?
toPostCondName :: String -> String  Deterministic 
Transform a name into a name of the corresponding prostcondition by adding the suffix "'post".
toPostCondQName :: (String,String) -> (String,String)  Deterministic 
Transform a qualified name into a name of the corresponding postcondition by adding the suffix "'post".
fromPostCondName :: String -> String  Deterministic 
Drop the postcondition suffix "'post" from the name:
isNonFailName :: String -> Bool  Deterministic 
Is this the name of a precondition?
toNonFailName :: String -> String  Deterministic 
Transform a name into a name of the corresponding prostcondition by adding the suffix "'post".
toNonFailQName :: (String,String) -> (String,String)  Deterministic 
Transform a qualified name into a name of the corresponding postcondition by adding the suffix "'post".
fromNonFailName :: String -> String  Deterministic 
Drop the postcondition suffix "'nonfail" from the name:
decodeContractQName :: (String,String) -> (String,String)  Deterministic 
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.
decodeContractName :: String -> String  Deterministic 
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.
encodeContractQName :: (String,String) -> (String,String)  Deterministic 
Transforms a qualified operation name of the form fn'tail into a valid identifier.
encodeContractName :: String -> String  Deterministic 
Transforms an operation name of the form fn'tail into a valid identifier.

Exported operations:

isSpecName :: String -> Bool  Deterministic 

Is this the name of a specification?

toSpecName :: String -> String  Deterministic 

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

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

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

fromSpecName :: String -> String  Deterministic 

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

isPreCondName :: String -> Bool  Deterministic 

Is this the name of a precondition?

toPreCondName :: String -> String  Deterministic 

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

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

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

fromPreCondName :: String -> String  Deterministic 

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

isPostCondName :: String -> Bool  Deterministic 

Is this the name of a precondition?

toPostCondName :: String -> String  Deterministic 

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

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

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

fromPostCondName :: String -> String  Deterministic 

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

isNonFailName :: String -> Bool  Deterministic 

Is this the name of a precondition?

toNonFailName :: String -> String  Deterministic 

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

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

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

fromNonFailName :: String -> String  Deterministic 

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

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

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  Deterministic 

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)  Deterministic 

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  Deterministic 

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.