An IDE for Symboleo, a formal contract specification language.
View the Project on GitHub Smart-Contract-Modelling-uOttawa/Symboleo-IDE
An IDE for the formal contract specification Symboleo is created using Xtext DSL generator. For installating and using the IDE, please take a look at the installation guide.
Symboleo is a formal contract specification language developed by Contract Specification and Modelling (CSM) Lab at Univeristy of Ottawa EECS department. The language aims to enable normative monitoring of smart contracts. Smart contracts are contracts that can monitor their performance (execution). They are a Cyber Physical System (CPS) that utilizes immutable ledgers (such as Distributed Ledger Technology (DLT) Platforms, a.k.a. blockchains).
For more information of Symboleo, please refer the preprint of our accepted paper for RE’20 conference here.
The current version of the text editor created by Xtext has implemented the syntax of Symboleo. It provides the capability to write Symboleo contract specifications more easily (autofill and syntax highlighting).
Create a New General Project (**File | New | Project… | General | Project**). |
.symboleo
extension.Ctrl
+ Space
to use autofill).
(Note2: the auto-fill feature might not suggest all the available options, as some of the grammar rules are implemented in a nested fashion).Basic Conepts | Ontological Concepts |
---|---|
Enumeration |
Event |
String |
Asset |
Number |
Role |
Date |
Contract |
Boolean |
Contract Body Element | Description | Allowable Inputs |
---|---|---|
Contract Signature |
contract template ID and contract parameters are defined | Contract ID & contract parameters and their type |
Declarations |
the parameters are bound to the variables which are defined based on the Domain Model of the contract |
var isA Type where att_1:=param_1 , … |
Preconditions |
the logical propositions that must be satisfied before a contract can be executed | logical proposition (Proposition ) |
Postconditions |
the logical propositions that must be satisfied after a contract is executed | logical proposition (Proposition ) |
Obligations |
obligations have a name, a trigger(optional), two roles, an antecedent and a consequent. the trigger when satisfied, creates an instance of the obligation, while satisfying its antecedent will bring it to an active state, i.e. the debtor of the obligation must satisfy the consequent. | oblName : trigger:Proposition -> O( debtor:Role , creditor:Role , antecedent:Proposition , consequent:Proposition ) |
Powers |
powers have a name, a trigger(optional), two roles, an antecedent and a consequent. the trigger when satisfied, creates an instance of the power, while satisfying its antecedent will bring it to an active state, i.e. the creditor of the power can satisfy the consequent which is usually about creating, suspending, resuming or terminating the obligations/contract. | powName : trigger:Proposition -> P( creditor:Role , debtor:Role , antecedent:Proposition , consequent:Proposition ) |
Constraints |
the logical propositions that must be always satisfied during the execution of the contract | logical proposition (Proposition ) |
Symboleo-IDE/samples/MeatSaleContract.symboleo
, illustrates how a simple contract can be specified in Symboleo.
```
Domain meatSaleDomain
Seller isA Role with returnAddress: String, name: String;
Buyer isA Role with warehouse: String;
Currency isAn Enumeration(CAD, USD, EUR);
MeatQuality isAn Enumeration(PRIME, AAA, AA, A);
PerishableGood isAn Asset with quantity: Number, quality: MeatQuality;
Meat isA PerishableGood;
Delivered isAn Event with item: Meat, deliveryAddress: String, delDueDate: Date;
Paid isAn Event with amount: Number, currency: Currency, from: Buyer, to: Seller, payDueDate: Date;
PaidLate isAn Event with amount: Number, currency: Currency, from: Buyer, to: Seller;
Disclosed isAn Event;
endDomainContract MeatSale (buyer : Buyer, seller : Seller, qnt : Number, qlt : MeatQuality, amt : Number, curr : Currency, payDueDate: Date, delAdd : String, effDate : Date, delDueDateDays : Number, interestRate: Number )
Declarations goods: Meat with quantity := qnt, quality := qlt; delivered: Delivered with item := goods, deliveryAddress := delAdd, delDueDate := Date.add(effDate, delDueDateDays, days); paidLate: PaidLate with amount := (1 + interestRate / 100) * amt, currency := curr, from := buyer, to := seller; paid: Paid with amount := amt, currency := curr, from := buyer, to := seller, payDueDate := payDueDate; disclosed: Disclosed;
Preconditions IsOwner(goods, seller);
Postconditions IsOwner(goods, buyer) and not(IsOwner(goods, seller));
Obligations delivery: Obligation(seller, buyer, true, WhappensBefore(delivered, delivered.delDueDate)); payment: O(buyer, seller , true, WhappensBefore(paid, paid.payDueDate)); latePayment: Happens(Violated(obligations.payment)) -> O(buyer, seller, true, Happens(paidLate));
//Surviving Obligations // so1 : Obligation(seller, buyer, true, not WhappensBefore(disclosed, Date.add(Activated(self), 6, months))); // so2 : Obligation(buyer, seller, true, not WhappensBefore(disclosed, Date.add(Activated(self), 6, months)));
Powers suspendDelivery : Happens(Violated(obligations.payment)) -> Power(seller, buyer, true, Suspended(obligations.delivery)); resumeDelivery: HappensWithin(paidLate, Suspension(obligations.delivery)) -> P(buyer, seller, true, Resumed(obligations.delivery)); terminateContract: Happens(Violated(obligations.delivery)) -> P(buyer, seller, true, Terminated(self));
Constraints not(IsEqual(buyer, seller)); CannotBeAssigned(suspendDelivery); CannotBeAssigned(resumeDelivery); CannotBeAssigned(terminateContract); CannotBeAssigned(delivery); CannotBeAssigned(payment); CannotBeAssigned(latePayment); delivered.delDueDate < paid.payDueDate;
endContract ```
Example of three contracts with their Symboleo specifications and generated smart contracts are avaialbe in another repository.