Pact shared with pact-web.

pact-web-share.pact

;;
;; Hi Doug, please find your favorite smart contract below.
;;
;; Best,
;; Robert

(define-keyset 'admin-keyset (read-keyset "admin-keyset"))

;; Define the module.
(module verificationDoug 'admin-keyset
  @doc "Little example to show off the usefulness of formal verification."

  (defun absBugDoug: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)
     )
   )
 )