• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
      • Defun
      • Verify-guards
      • Table
      • Mutual-recursion
      • Memoize
      • Make-event
      • Include-book
      • Encapsulate
      • Defun-sk
      • Defttag
      • Defstobj
      • Defpkg
      • Defattach
      • Defchoose
      • Defabsstobj
      • Progn
      • Verify-termination
      • Redundant-events
      • Defconst
      • Defmacro
      • Skip-proofs
      • In-theory
      • Embedded-event-form
      • Value-triple
      • Comp
      • Local
      • Defthm
      • Progn!
      • Defevaluator
      • Theory-invariant
      • Assert-event
      • Defun-inline
      • Project-dir-alist
      • Partial-encapsulate
      • Define-trusted-clause-processor
      • Defproxy
      • Defexec
      • Defun-nx
      • Defthmg
      • Defpun
      • Defabbrev
      • Set-table-guard
      • Name
      • Defrec
      • Add-custom-keyword-hint
      • Regenerate-tau-database
      • Defcong
      • Deftheory
      • Deftheory-static
      • Defaxiom
      • Defund
      • Evisc-table
      • Verify-guards+
      • Logical-name
      • Profile
      • Defequiv
      • Defmacro-untouchable
      • Defthmr
      • Add-global-stobj
      • Defstub
      • Defrefinement
      • Deflabel
      • In-arithmetic-theory
      • Unmemoize
      • Defabsstobj-missing-events
      • Defthmd
      • Fake-event
      • Set-body
      • Defun-notinline
      • Functions-after
      • Macros-after
      • Dump-events
      • Defund-nx
      • Defun$
      • Remove-custom-keyword-hint
      • Dft
      • Defthy
      • Remove-global-stobj
      • Defund-notinline
      • Defnd
      • Defn
      • Defund-inline
      • Defmacro-last
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Events
• Stobj

Add-global-stobj

Add a global stobj with a given name

See stobj for background on stobjs, and see defstobj and defabsstobj for further background.

We start with the General Form and an Example Form, which are followed by discussions of global stobjs and the effect of this utility.

General Form:
(add-global-stobj x state)

where x evaluates to the name of a stobj that does not already have a global value, either because it was introduced by defstobj or defabsstobj with keyword value :non-executable t or because remove-global-stobj was previously applied to that name.

Example Form:
(add-global-stobj 'st state) ; st non-global from defstobj or defabsstobj

By default, defstobj and defabsstobj create a “live”, mutable object for the given name that can be referenced at the top level, which we call a “global” stobj. This is illustrated by the following log.

ACL2 !>(defstobj st fld)

Summary
Form:  ( DEFSTOBJ ST ...)
Rules: NIL
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
 ST
ACL2 !>st ; global stobj for the name, ST
<st>
ACL2 !>(fld st)
NIL
ACL2 !>(update-fld 3 st)
<st>
ACL2 !>(fld st)
3
ACL2 !>

However, the following log shows that we can introduce a stobj without creating a global stobj, by using the keyword value :non-executable t.

ACL2 !>(defstobj st2 fld2 :non-executable t)

Summary
Form:  ( DEFSTOBJ ST2 ...)
Rules: NIL
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
 ST2
ACL2 !>(fld2 st2)


ACL2 Error [Evaluation] in TOP-LEVEL:  Unbound var ST2.  Note that
ST2 is a non-executable stobj.

ACL2 !>

The function add-global-stobj creates a global stobj for a given stobj name when one does not already exist. Let's continue the log started immediately above.

ACL2 !>(add-global-stobj 'st2 state)
 ST2
ACL2 !>(fld2 st2)
NIL
ACL2 !>(update-fld2 3 st2)
<st2>
ACL2 !>(fld2 st2)
3
ACL2 !>

The function remove-global-stobj removes the indicated global stobj. We continue the log above.

ACL2 !>(remove-global-stobj 'st2 state)
 ST2
ACL2 !>(fld2 st2)


ACL2 Error [Evaluation] in TOP-LEVEL:  Unbound var ST2.  Note that
ST2 is a non-executable stobj.

ACL2 !>

If we remove a global stobj, as shown just above, and then add the corresponding global stobj, we get a fresh copy of that stobj; all previous updates are discarded.

ACL2 !>(add-global-stobj 'st2 state)
 ST2
ACL2 !>(fld2 st2)
NIL
ACL2 !>