This contract is the archetype version of the contract taken from the Findel paper (Financial Derivatives Language).
Suppose Alice sells to Bob a zero-coupon (i.e., paying no interest) bond that pays $11 in one year for $10.
The findel expression below describes this contract:
And ( Give( Scale( 10; One( USD ))); At( now+1 years; Scale( 11 ; One( USD ))))
zero_coupon_bond.arlarchetype zero_coupon_bondvariable issuer : role = @tz1bfVgcJC4ukaQSHUe1EbrUd5SekXeP9CWk (* seller 'Alice' *)variable owner : role = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg(* buyer 'Bob'; receives 11 tez in one-year *)variable price : tez = 10tzvariable payment : tez = 1.1 * pricevariable maturity : date = 2020-12-31states =| Created initial| Confirmed (* owner has purchased bond *)| Repaid (* issuer has transferred payment to contract *)| Collected (* owner has collected payment *)transition confirm () {specification {postcondition s1 {balance = 0tz}}from Createdto Confirmedwhen { transferred = price }with effect {maturity := now + 365d;transfer price to issuer}}transition repay () {called by issuerfrom Confirmedto Repaid when { transferred = payment }}transition collect () {called by ownerfrom Repaidto Collectedwhen { now >= maturity }with effect {if balance >= paymentthen transfer balance to owner}}