• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
    • Start-here
      • Gentle-introduction-to-ACL2-programming
      • ACL2-tutorial
        • Introduction-to-the-theorem-prover
        • Pages Written Especially for the Tours
          • A Tiny Warning Sign
          • About the Prompt
          • ACL2 Symbols
          • Common Lisp
          • About Types
          • The Event Summary
          • An Example of ACL2 in Use
          • The Tours
          • Corroborating Models
          • The Proof of the Associativity of App
          • Guards in ACL2
          • Numbers in ACL2
          • About the Admission of Recursive Definitions
          • Free Variables in Top-Level Input
          • Common Lisp as a Modeling Language
          • ACL2 as an Interactive Theorem Prover (cont)
          • A Flying Tour of ACL2
          • Analyzing Common Lisp Models
          • A Walking Tour of ACL2
          • The Theorem that App is Associative
          • The End of the Walking Tour
          • Proving Theorems about Models
          • Functions for Manipulating these Objects
          • About the ACL2 Home Page
          • ACL2 Conses or Ordered Pairs
          • The Associativity of App
          • Models of Computer Hardware and Software
          • How To Find Out about ACL2 Functions (cont)
          • A Sketch of How the Rewriter Works
          • ACL2 System Architecture
          • Running Models
          • ACL2 is an Untyped Language
          • How To Find Out about ACL2 Functions
          • How Long Does It Take to Become an Effective User(Q)
          • The Admission of App
          • Guiding the ACL2 Theorem Prover
          • What Is ACL2(Q)
          • Conversion
          • An Example Common Lisp Function Definition
          • ACL2 Characters
          • You Must Think about the Use of a Formula as a Rule
          • The WARNING about the Trivial Consequence
          • Guessing the Type of a Newly Admitted Function
          • ACL2 Strings
          • What is a Mathematical Logic(Q)
          • Revisiting the Admission of App
          • What is a Mechanical Theorem Prover(Q)
          • About Models
          • What is Required of the User(Q)
          • Hey Wait! Is ACL2 Typed or Untyped(Q)
          • The Falling Body Model
          • Rewrite Rules are Generated from DEFTHM Events
          • A Typical State
          • The Time Taken to do the Associativity of App Proof
          • The Simplification of the Induction Conclusion (Step 1)
          • The Rules used in the Associativity of App Proof
          • Subsumption of Induction Candidates in App Example
          • Other Requirements
          • Models in Engineering
          • Symbolic Execution of Models
          • Suggested Inductions in the Associativity of App Example
          • Overview of the Proof of a Trivial Consequence
          • Evaluating App on Sample Input
          • The Induction Step in the App Example
          • Modeling in ACL2
          • The Simplification of the Induction Conclusion (Step 9)
          • The Induction Scheme Selected for the App Example
          • The First Application of the Associativity Rule
          • Overview of the Expansion of ENDP in the Induction Step
          • Flawed Induction Candidates in App Example
          • ACL2 as an Interactive Theorem Prover
          • Using the Associativity of App to Prove a Trivial Consequence
          • The Simplification of the Induction Conclusion (Step 8)
          • The Instantiation of the Induction Scheme
          • The Final Simplification in the Base Case (Step 0)
          • Overview of the Simplification of the Induction Step to T
          • Overview of the Simplification of the Induction Conclusion
          • On the Naming of Subgoals
          • Nontautological Subgoals
          • What is a Mechanical Theorem Prover(Q) (cont)
          • The Simplification of the Induction Conclusion (Step 12)
          • The Simplification of the Induction Conclusion (Step 10)
          • The End of the Flying Tour
          • The Base Case in the App Example
          • The Simplification of the Induction Conclusion (Step 11)
          • The Final Simplification in the Base Case (Step 3)
          • The Expansion of ENDP in the Induction Step (Step 1)
          • The Expansion of ENDP in the Induction Step (Step 0)
          • The End of the Proof of the Associativity of App
          • Overview of the Simplification of the Base Case to T
          • The Summary of the Proof of the Trivial Consequence
          • The Simplification of the Induction Conclusion (Step 7)
          • The Simplification of the Induction Conclusion (Step 6)
          • The Simplification of the Induction Conclusion (Step 5)
          • The Simplification of the Induction Conclusion (Step 4)
          • The Simplification of the Induction Conclusion (Step 2)
          • The Simplification of the Induction Conclusion (Step 0)
          • The Justification of the Induction Scheme
          • The Final Simplification in the Base Case (Step 1)
          • The Expansion of ENDP in the Induction Step (Step 2)
          • Popping out of an Inductive Proof
          • Overview of the Expansion of ENDP in the Base Case
          • The Simplification of the Induction Conclusion (Step 3)
          • The Q.E.D. Message
          • Overview of the Final Simplification in the Base Case
          • The Final Simplification in the Base Case (Step 2)
          • Perhaps
          • Name the Formula Above
          • Undocumented Topic
          • A Trivial Proof
        • The-method
        • Advanced-features
        • Interesting-applications
        • Tips
        • Alternative-introduction
        • Tidbits
        • Annotated-ACL2-scripts
        • Startup
        • ACL2-as-standalone-program
        • ACL2-sedan
        • Talks
        • Nqthm-to-ACL2
        • Emacs
      • About-ACL2
    • Real
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Pages Written Especially for the Tours

Functions for Manipulating these Objects

Functions for Manipulating these Objects

Consider a typical ``stack'' of control frames.

Suppose the model required that we express the idea of ``the most recent frame whose return program counter points into MAIN.''

The natural expression of this notion involves

function application — ``fetch the return-pc of this frame''

case analysis — ``if the pc is MAIN, then ...''

iteration or recursion — ``pop this frame off and repeat.''

The designers of ACL2 have taken the position that a programming language is the natural language in which to define such notions, provided the language has a mathematical foundation so that models can be analyzed and properties derived logically.

Common Lisp is the language supported by ACL2. To be precise, a small applicative subset of Common Lisp is the language supported by ACL2.