Skip to content

Instantly share code, notes, and snippets.

@mightybyte
Created April 15, 2019 17:32
Show Gist options
  • Save mightybyte/33c290da70a25db8c83da9388118ae33 to your computer and use it in GitHub Desktop.
Save mightybyte/33c290da70a25db8c83da9388118ae33 to your computer and use it in GitHub Desktop.
Pact formal verification example
;;
;; A little example showing off the merits of formal
;; verification and why it pays off.
;;
;; Keysets cannot be created in code, thus we read them in
;; from the load message data.
(define-keyset 'admin-keyset (read-keyset "admin-keyset"))
;; Define the module.
(module verification 'admin-keyset
@doc "Little example to show off the usefulness of formal verification."
(defun absBug:integer (num:integer)
@doc "Ensure positive result"
;; This property fails: Would you have caught that with unit tests?
@model [(property (>= result 0))]
(if (= (- (* (- num 6) (+ num 11)) (* 42 num)) (* (* 64 7) 52270780833))
(- 1)
(abs num)
)
)
)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment