Defunc
Function definitions with contracts. See also
definec and defun.
Examples
(defunc len (a)
:input-contract t
:output-contract (natp (len a))
(if (atom a)
0
(+ 1 (len (rest a)))))
(defunc app (x y)
:input-contract (and (true-listp x) (true-listp y))
:output-contract (and (true-listp (app x y))
(equal (len (app x y)) (+ (len x) (len y))))
(if (endp x)
y
(cons (car x) (app (cdr x) y))))
(defunc add-digits (x)
:input-contract (natp x)
:output-contract (natp (add-digits x))
:function-contract-hints (("Goal" :do-not '(acl2::generalize)))
(if (< x 10)
x
(let* ((rem (rem x 10))
(y (/ (- x rem) 10)))
(+ rem (add-digits y)))))
(defunc square-list (l)
:input-contract (nat-listp l)
:output-contract (nat-listp (square-list l))
(if (endp l)
nil
(app (list (* (car l) (car l)))
(square-list (cdr l))))
:verbose t
:skip-tests t)
Purpose
The macro defunc is an extension of defun with
contracts. We recommend the use of definec, a macro based
on defunc, which is as powerful as defunc, but allows one to
write more concise definitions.
Using defunc one can specify input and output
contracts (pre and post conditions) for a function. The following
actions are performed when defunc is used in the default
way. If any of the actions fail, then an informative error
message is printed. If all actions succeed, then the function has
been successfully admitted to ACL2s.
- Test the function contract, i.e., whether the output
contract holds under the assumption that the function terminates
and the input contract holds.
- Test the body contracts, i.e., whether the contracts of the
functions appearing in the body of the defunc are violated.
- Construct a definition in the core ACL2 logic that respects
the input contracts, and prove that this definition is
terminating.
- Prove the function contract, i.e., that the input
contract implies the output contract.
- Prove the body contracts, i.e., that for each occurrence of
a function call inside the body of the function being defined,
all of the arguments to the function call satisfy the input
contracts of the function. In ACL2 parlance, this is guard
verification.
- Replace the function definition and induction scheme with a
definition rule and an induction scheme for the function that
restricts definition expansion and inductions to contexts where
the input contract is satisfied. If defunc is used in a
disciplined way, then all contexts should satisfy this
restriction. Use :pcb fun-name to check the names of the
above events.
Syntax
The general form of defunc is:
(defunc name (x1 x2 ...)
[doc-string declare-form*]
[:input-contract ic]
[:output-contract oc]
[:function-contract-hints hints :rule-classes ...] ;function contract hints
[:body-contracts-hints hints] ;body contracts hints
[Other :key value ...]
body)
The form of defunc is just like defun except that is allows
extra keyword options. Note that the keyword options can go anywhere
between the formals (parameters) and the end of defunc macro.
The supported keyword options with the syntax restrictions and actions are noted
below.
Keyword Options
- :input-contract ic
- Required; ic is a term.
- :output-contract oc
- Required; oc is a term.
- :function-contract-hints hints
- Passed as :hints to the
function contract defthm.
- :rule-classes rcs
:instructions is
:otf-flg flg
- These three keyword arguments are passed directly to the function
contract defthm.
- :body-contracts-hints hints
- Passed as :hints to the
body contracts defthm.
The following keyword options are usually set at the
session-wide-level (see the set-defunc-* macros documented
below); when given as keyword arguments to defunc they override
the session defaults.
- :termination-strictp x
- When x is t (default), abort if termination failed.
- When x is nil, then if termination fails, admit the function in
:program mode.
- :function-contract-strictp x
- When x is t (default), abort if the contract proof failed.
- When x is nil, then if the proof fails, add a dynamic contract
check.
- :body-contracts-strictp x
- When x is t (default), abort if the body contracts proof
failed.
- When x is nil, body contracts are checked dynamically.
- :timeout n
- Limit the time spent in defunc events to n seconds.
- :skip-tests t
- Skip the testing actions.
Debugging
To debug a failed defunc form, you can proceed in multiple ways:
- Submit the events shown above the failure message to replicate the error.
- At the session editor (or emacs prompt), submit/evaluate
:trans1 (defunc ...)
And from the output, evaluate the form that says (defunc-events ...).
- Use keyword options :verbose t (or :debug t) and examine the ACL2 output.
Subtopics
- Definec
- Function definitions with contracts extending defunc.
- Set-defunc-termination-strictp
- Set termination-strictp for defunc
- Set-defunc-timeout
- Set timeout (in seconds) for defunc
- Set-defunc-function-contract-strictp
- Set function-contract-strictp for defunc
- Set-defunc-force-ic-hyps-in-definitionp
- Set force-ic-hyps-in-definitionp for defunc
- Set-defunc-force-ic-hyps-in-contract-thmp
- Set force-ic-hyps-in-contract-thmp for defunc
- Set-defunc-body-contracts-strictp
- Set body-contracts-strictp for defunc
- Get-defunc-timeout
- Get timeout default for defunc
- Get-defunc-termination-strictp
- Get termination-strictp default for defunc
- Get-defunc-function-contract-strictp
- Get function-contract-strictp default for defunc
- Get-defunc-force-ic-hyps-in-definitionp
- Get force-ic-hyps-in-definitionp default for defunc
- Get-defunc-force-ic-hyps-in-contract-thmp
- Get force-ic-hyps-in-contract-thmp default for defunc
- Get-defunc-body-contracts-strictp
- Get body-contracts-strictp default for defunc
