Created
June 5, 2019 21:54
-
-
Save sirlensalot/c1c55c5647e744525545a3240c0da858 to your computer and use it in GitHub Desktop.
Pact shared with pact-web.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
;; | |
;; "Hello, world!" smart contract/module | |
;; | |
;; To try it out, click "Load into REPL" and type into the repl: | |
;; pact> (hello-world.greet) | |
;; | |
;; Check lines 21 and 34 to play with Formal Verification | |
;; | |
;; Define the module. | |
(module hello-world MODULE_ADMIN | |
"A smart contract to greet the world." | |
; no-op module admin for example purposes. | |
; in a real contract this could enforce a keyset, or | |
; tally votes, etc. | |
(defcap MODULE_ADMIN () true) | |
(defschema message-schema | |
@doc "Message schema" | |
@model [(invariant (!= msg ""))] | |
msg:string) | |
(deftable | |
message:{message-schema}) | |
(defun set-message | |
( | |
m:string | |
) | |
"Set the message that will be used next" | |
; uncomment the following to make the model happy! | |
; (enforce (!= m "") "set-message: must not be empty") | |
(write message "0" {"msg": m}) | |
) | |
(defun greet () | |
"Do the hello-world dance" | |
(with-default-read message "0" { "msg": "" } { "msg":= msg } | |
(format "Hello {}!" [msg]))) | |
) | |
(create-table message) | |
(set-message "world") | |
(greet) | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment