Scilla Contractの構造

Scillaのコントラクトは、LibraryとContractの2部で構成され、Libraryから始まります。

その次にContractが定義されます。

Contract内は大きく３構造となります。

変更不可なContractのパラメータ宣言

変更可なフィールド変数の宣言

変更不可な変数

変更不可なパラメータはContract初期パラメータとなっており、Contract作成時に定義され、それ以降変更できません。

変数はContract作成時に指定する必要があります。

(vname_1 : vtype_1,

vname_2 : vtype_2,

... )

変更可な変数

変更可な変数はContractの変更可能な状態を表します。

field vname_1 : vtype_1 = expr_1

field vname_2 : vtype_2 = expr_2

トランジション

code:MyContract

(* Scilla contract structure *)

(***************************************************)

(* Associated library *)

(***************************************************)

library MyContractLib

(* Library code block follows *)

(***************************************************)

(* Contract definition *)

(***************************************************)

contract MyContract

(* Immutable fields declaration *)

(vname_1 : vtype_1,

vname_2 : vtype_2)

(* Mutable fields declaration *)

field vname_1 : vtype_1 = init_val_1

field vname_2 : vtype_2 = init_val_2

(* Transitions *)

(* Transition signature *)

transition firstTransition (param_1 : type_1, param_2 : type_2)

(* Transition body *)

end

transition secondTransition (param_1: type_1)

(* Transition body *)

end