• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
      • Open-channel-lemmas
      • Std/io/read-char$
      • Std/io/read-object
      • Std/io/open-output-channel
      • Unsound-read
      • Read-string
      • Read-bytes$
      • File-measure
      • Read-bytes$-n
      • Std/io/read-byte$
      • Std/io/open-input-channel
      • Print-compressed
      • Read-file-lines-no-newlines
      • Nthcdr-bytes
      • Read-file-lines
      • Std/io/close-output-channel
      • Read-file-characters
      • Read-file-bytes
      • Print-legibly
      • Std/io/close-input-channel
      • Read-file-objects
      • Logical-story-of-io
      • Take-bytes
      • Std/io/peek-char$
      • Read-file-characters-rev
      • Read-file-as-string
      • Std/io/write-byte$
      • Std/io/set-serialize-character
      • Std/io/print-object$
      • Std/io/princ$
      • Std/io/read-file-into-string
      • *file-types*
    • Std/osets
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Std/io
• Close-output-channel

Std/io/close-output-channel

Close an output channel.

Signature: (close-output-channel channel state-state) returns state.

• channel is a symbol that must refer to a currently open output channel; see open-output-channel.
• state is the ACL2 state.

This is a logic-mode function, but its logical definition is tricky; see logical-story-of-io. The main logical consequence is that channel will no longer be an open output channel, and hence can no longer be written to or closed.

Under the hood, we close the raw Lisp stream associated with channel. This typically involves flushing the buffers associated with the file (i.e., actually writing your output to disk). It is generally necessary to close output channels when you are done with them to avoid resource leaks.

Definitions and Theorems

Theorem: state-p1-of-close-output-channel-free

(defthm state-p1-of-close-output-channel-free
        (implies (and (open-output-channel-p1 channel type state)
                      (state-p1 state))
                 (state-p1 (close-output-channel channel state))))

Theorem: state-p1-of-close-output-channel-types

(defthm state-p1-of-close-output-channel-types
        (implies (and (or (open-output-channel-p1 channel
                                                  :byte state)
                          (open-output-channel-p1 channel
                                                  :object state)
                          (open-output-channel-p1 channel
                                                  :character state))
                      (state-p1 state))
                 (state-p1 (close-output-channel channel state))))

Theorem: state-p1-of-close-output-channel-of-open

(defthm
 state-p1-of-close-output-channel-of-open
 (implies
     (and (open-output-channel-p1
               (mv-nth 0
                       (open-output-channel fname type state1))
               type state)
          (state-p1 state))
     (state-p1 (close-output-channel
                    (mv-nth 0
                            (open-output-channel fname type state1))
                    state))))