Filtering...

properties-testing

books/acl2s/properties-testing
other
(in-package "ACL2S")
other
(include-book "acl2s/ccg/ccg" :uncertified-okp nil :dir :system :ttags ((:ccg)) :load-compiled-file nil)
other
(include-book "acl2s/base-theory" :dir :system :ttags :all)
other
(include-book "acl2s/custom" :dir :system :ttags :all)
other
(acl2s-defaults :set cgen-single-test-timeout
  0)
other
(property (n :nat)
  (booleanp (nth-boolean-builtin n)))
other
(property (n :nat)
  :proofs? nil
  (booleanp (nth-boolean-builtin n)))
other
(property (n :nat)
  :testing? nil
  (booleanp (nth-boolean-builtin n)))
other
(property (n :nat)
  :proofs? nil
  :testing? nil
  (booleanp (nth-boolean-builtin n)))
other
(property (n :nat)
  (natp (+ 1 n))
  :hints (("goal" :do-not '(preprocess))))
other
(must-fail (property (n :nat)
    (natp (+ 1 n))
    :hints (("goal" :do-not '(pre--process)))))
other
(must-fail (property (n :nat)
    :testing? nil
    (natp (+ 1 n))
    :hints (("goal" :do-not '(pre--process)))))
other
(property (n :nat)
  (negp (nth-neg-builtin n)))
other
(property (n :nat)
  (non-pos-integerp (nth-non-pos-integer-builtin n)))
other
(property (n :nat)
  (non-0-integerp (nth-non-0-integer-builtin n)))
other
(property (n :nat)
  (integerp (nth-integer-builtin n)))
other
(property (n :nat lo hi :int)
  :h (<= lo hi)
  :b (and (integerp (nth-integer-between n lo hi))
    (<= lo
      (nth-integer-between n lo hi))
    (>= hi
      (nth-integer-between n lo hi))))
other
(property (n :nat)
  :check-contracts? nil
  :proofs? nil
  (pos-ratiop (nth-pos-ratio-builtin n)))
other
(property (n :nat)
  :check-contracts? nil
  :proofs? nil
  (neg-ratiop (nth-neg-ratio-builtin n)))
other
(property (n :nat)
  (neg-rationalp (nth-neg-rational-builtin n)))
other
(property (n :nat)
  (pos-rationalp (nth-pos-rational-builtin n)))
other
(property (n :nat)
  (non-neg-rationalp (nth-non-neg-rational-builtin n)))
other
(property (n :nat)
  (non-pos-rationalp (nth-non-pos-rational-builtin n)))
other
(property (n :nat)
  (non-0-rationalp (nth-non-0-rational-builtin n)))
other
(property (n :nat)
  (rationalp (nth-rational-builtin n)))
other
(property (n :nat lo hi :rational)
  :proofs? nil
  :h (<= lo hi)
  :b (and (rationalp (nth-rational-between n lo hi))
    (<= lo
      (nth-rational-between n lo hi))
    (>= hi
      (nth-rational-between n lo hi))))
other
(defdata one 1)
other
(defdata loi (listof int))
other
(defdata r1
  (record (a . loi)))
other
(defdata data (listof nat))
other
(defdata receiver-state
  (record (received . data)))
other
(definec bax
  (rs :data)
  :receiver-state (receiver-state rs))
other
(property (lo hi :int n :nat)
  :check-contracts? nil
  :h (<= lo hi)
  :b (^ (<= lo
      (geometric-int-between lo hi n))
    (>= hi
      (geometric-int-between lo hi n))))
other
(property (lo hi :rational n :nat)
  :check-contracts? nil
  :h (<= lo hi)
  (^ (<= lo
      (geometric-rat-between lo hi n))
    (>= hi
      (geometric-rat-between lo hi n))))
other
(property (lo hi :int)
  :check-contracts? nil
  :test-contracts? nil
  :proofs? nil
  :h (<= lo hi)
  (b* (((mv mid1 mid2) (int-midpoints lo hi)))
    (^ (<= lo mid1)
      (>= hi mid2))))
other
(property (lo hi :rational)
  :check-contracts? nil
  :test-contracts? nil
  :h (<= lo hi)
  (b* (((mv mid1 mid2) (rat-midpoints lo hi)))
    (^ (<= lo mid1)
      (>= hi mid2))))