The process of translation of a contract in natural language into a formal specification requires to perform the following steps. In the first step, semantic annotation is performed to identify the different contract concepts of a contract (e.g., roles, obligations, conditions, etc.) or concerning the identification of the structural elements of the contract (e.g., clause, title). Semantic annotation lead to the identification of the following concepts. The annotation process is defined in terms of the paper (ContracT PoEM reference).

Subsequently the relationships between the different elements of the contact are identified. For each power and obligation 5 different elements have to be identified: trigger, antecedent, consequent, debtor and creditor. The elements identified are defined as such in the process:

A few elements can be reused for the identification of contract elements in step number two: debtors and creditors represents roles that are identified in the step of semantic annotation. Triggers, antecedent and consequent are situations and are expressed in boolean terms. Not every element is specificied for every power and obligation and may be added manually to fully identify relationships. As a general note, not every element is used in the subsequent step but they will be necessary for subsequent steps. As such, to ease the identification of requirements for each steps, a mapping has been integrated in the process, in order to identify how every single element determined and identified in each step is reused in one or more subsequent steps of the process. The identification antecedent, consequent and triggers can be supported by the annotation step. For example, based on recurring patterns that could determine a a casualty relationship to identify triggers and that in the legal ontology have been called “events” and in which antecedent and consequent may refer to pre-state and post-state obligations. Concerning contract automation and more specifically with the development of smart contracts in general (e.g., including ChainCode in Hyperledger), the concept of event is mostly used to define what in our approach is defined as trigger.

The third phase, related to the identification of a domain model, is composed by two sub-steps. In a first step, variables and parameters are identified. In our definition, a variable is a container for a specific type of data, like integer, float, string, etc. A parameter is the value assigned to the the variable. In the second sub-step, the domain model is defined that categorizes the contract elements into the legal ontology adapted. With a contract automation objective, parameters and local variables has to be modified to make it fit for the contract being analyzed, similarly to contract templates frequently available for recurring contracts (e.g., rental of an house). In the meat contract, such elements are referring to the quantity of the meat, the quality, dates, prices, interest rates and days concerning the right to terminate. “Is a” represents a subclass of a more general class. A relevant part of the elements identified in the domain model are the elements identified with semantic annotation (e.g., seller, buyer, asset). Moreover, the identification of parameters and named variables can potentially be based on the grammar that has been defined in the first step for semantic annotation (e.g., amount, currency, weight, distance, unit). Similarly, the grammar identified for structure annotation can be used (e.g., name, dates, contract identifier). The domain model represents, in a way, the specialization of the ontology for the specific contract being analyzed. The elements of the domain model can be generally divided into three categories: 1) the parties involved in the contract (e.g., Seller and Buyer), 2) the exchange representing the substance of the contract (e.g. meat versus monetary payment) and the 3) events that are arising from the perfomance of the contract (e.g. delivered, paid, paid late, disclosed)

The fourth step refers to the generation of the formal specification which entails 1) the domain section, already identified in the previous step, contains domain-dependent concepts and axioms and the specializations of Symboleo’s primitive concepts, and corresponds to the definitions stated in contracts. 2) The contract body which represents the core of the contract specifying its objective and which is composed by the following elements:

• Variables and parameters are initiated and can be reused from the section concerning the step for the identification of the domain model. They contain names and typed parameters

• Obligations and powers: those are composed of the elements that are identified in the second step of the process concerning the identification of relationships and is comprised of (debtor, creditor, antecedent, consequent, trigger). Similarly concerning powers the same concepts are identified in the process. The structure of the formal specification is defined by the elements identified in the second step of the process and as such, it determines Debtor, Creditor, the Antecedent that has been satisfied, expressed as “True”, even though such antecedent may not necessarily exist. Subsequently, the Consequent is substantiated, implying the obbligation (“happens”) or the negation of the obligation (“not happens”) or refers to temporal elements (“happens within”) that derive from the obligation or power. Those are instantiating the implications that are detailed in the Declaration section. The structure of the formal specification concerning each obligation and power is different if in the second step of the process, a trigger it has been identified or not. In the case in which a trigger has been identified, the formal specification refers, at first, to the obligation which lead to the trigger (e.g., in case of the meat contract, the failure to comply with the obligation to pay within ten days, may trigger the power of the Seller to terminate the contract). Subsequently, the the consequences derived from the trigger are specified. A surviving obligation is a specialization of an obligation and are surviving after the end of the contract (e.g., Non Disclosure greement (NDA)),

• Preconditions and postconditions represent conditions that have to be true before and after the execution of the contract, respectively

• Constraints are similarly conditions that have to hold true as the contract is being executed. For example, buyer and seller cannot represent the same entity, the contract has to be terminated in a predetermined period of time or obligations cannot be reassigned during contract execution. Most of the times, such elements are not made explicit in the contract. For the example of the meat contract, this implies that at least two parties are identified in the process.