• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
    • Io
    • Defttag
    • Sys-call
    • Save-exec
    • Quicklisp
    • 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
      • Read-file-lines-no-newlines
      • Print-compressed
      • 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*
    • Oslib
    • Bridge
    • Clex
    • Tshell
    • Unsound-eval
    • Hacker
    • ACL2s-interface
    • Startup-banner
    • Command-line
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Std/io

Open-channel-lemmas

Lemmas about when various state-modifying functions do and don't affect the list of open channels.

When programming with I/O, you may need to write functions that modify state in some way (perhaps by doing I/O) and exit returning a state which has some channels open, perhaps for further reading and writing later in your program. Then, to prove guard theorems elsewhere, you'll need returns theorems about your function showing that those channels are open, either because they were open before the function ran and the function didn't close them, or because the function itself opened them.

This book contains lemmas that can help you prove such returns theorems. For each built-in I/O function, there is a lemma saying that, under appropriate hypotheses, it doesn't close your open input or output channels.

Definitions and Theorems

First are lemmas about open-input-channel-p1.

Theorem: open-input-channel-p1-under-open-input-channel

(defthm open-input-channel-p1-under-open-input-channel
  (implies (open-input-channel-p1 channel type state)
           (b* (((mv other-channel state)
                 (open-input-channel fname other-type state)))
             (implies (implies (equal other-channel channel)
                               (equal other-type type))
                      (open-input-channel-p1 channel type state)))))

Theorem: open-input-channel-p1-under-open-output-channel

(defthm open-input-channel-p1-under-open-output-channel
  (implies (open-input-channel-p1 channel type state)
           (b* (((mv & state)
                 (open-output-channel fname other-type state)))
             (open-input-channel-p1 channel type state))))

Theorem: open-input-channel-p1-under-close-input-channel

(defthm open-input-channel-p1-under-close-input-channel
  (implies (and (open-input-channel-p1 channel type state)
                (not (equal channel other-channel)))
           (b* ((state (close-input-channel other-channel state)))
             (open-input-channel-p1 channel type state))))

Theorem: open-input-channel-p1-under-close-output-channel

(defthm open-input-channel-p1-under-close-output-channel
  (implies (open-input-channel-p1 channel type state)
           (b* ((state (close-output-channel other-channel state)))
             (open-input-channel-p1 channel type state))))

Theorem: open-input-channel-p1-under-read-char$

(defthm open-input-channel-p1-under-read-char$
  (implies (open-input-channel-p1 channel type state)
           (b* (((mv & state)
                 (read-char$ other-channel state)))
             (open-input-channel-p1 channel type state))))

Theorem: open-input-channel-p1-under-read-byte$

(defthm open-input-channel-p1-under-read-byte$
  (implies (open-input-channel-p1 channel type state)
           (b* (((mv & state)
                 (read-byte$ other-channel state)))
             (open-input-channel-p1 channel type state))))

Theorem: open-input-channel-p1-under-read-object

(defthm open-input-channel-p1-under-read-object
  (implies (open-input-channel-p1 channel type state)
           (b* (((mv & & state)
                 (read-object other-channel state)))
             (open-input-channel-p1 channel type state))))

Theorem: open-input-channel-p1-under-princ$

(defthm open-input-channel-p1-under-princ$
  (implies (open-input-channel-p1 channel type state)
           (b* ((state (princ$ x other-channel state)))
             (open-input-channel-p1 channel type state))))

Theorem: open-input-channel-p1-under-write-byte$

(defthm open-input-channel-p1-under-write-byte$
  (implies (open-input-channel-p1 channel type state)
           (b* ((state (write-byte$ byte other-channel state)))
             (open-input-channel-p1 channel type state))))

Theorem: open-input-channel-p1-under-print-object$

(defthm open-input-channel-p1-under-print-object$
  (implies (open-input-channel-p1 channel type state)
           (b* ((state (print-object$ byte other-channel state)))
             (open-input-channel-p1 channel type state))))

Theorem: open-input-channel-p1-under-set-serialize-character

(defthm open-input-channel-p1-under-set-serialize-character
  (implies (open-input-channel-p1 channel type state)
           (b* ((state (set-serialize-character c state)))
             (open-input-channel-p1 channel type state))))

Next are lemmas about open-output-channel-p1.

Theorem: open-output-channel-p1-under-open-input-channel

(defthm open-output-channel-p1-under-open-input-channel
  (implies (open-output-channel-p1 channel type state)
           (b* (((mv & state)
                 (open-input-channel fname other-type state)))
             (open-output-channel-p1 channel type state))))

Theorem: open-output-channel-p1-under-open-output-channel

(defthm open-output-channel-p1-under-open-output-channel
 (implies (open-output-channel-p1 channel type state)
          (b* (((mv other-channel state)
                (open-output-channel fname other-type state)))
            (implies (implies (equal other-channel channel)
                              (equal other-type type))
                     (open-output-channel-p1 channel type state)))))

Theorem: open-output-channel-p1-under-close-input-channel

(defthm open-output-channel-p1-under-close-input-channel
  (implies (open-output-channel-p1 channel type state)
           (b* ((state (close-input-channel other-channel state)))
             (open-output-channel-p1 channel type state))))

Theorem: open-output-channel-p1-under-close-output-channel

(defthm open-output-channel-p1-under-close-output-channel
  (implies (and (open-output-channel-p1 channel type state)
                (not (equal channel other-channel)))
           (b* ((state (close-output-channel other-channel state)))
             (open-output-channel-p1 channel type state))))

Theorem: open-output-channel-p1-under-read-char$

(defthm open-output-channel-p1-under-read-char$
  (implies (open-output-channel-p1 channel type state)
           (b* (((mv & state)
                 (read-char$ other-channel state)))
             (open-output-channel-p1 channel type state))))

Theorem: open-output-channel-p1-under-read-byte$

(defthm open-output-channel-p1-under-read-byte$
  (implies (open-output-channel-p1 channel type state)
           (b* (((mv & state)
                 (read-byte$ other-channel state)))
             (open-output-channel-p1 channel type state))))

Theorem: open-output-channel-p1-under-read-object

(defthm open-output-channel-p1-under-read-object
  (implies (open-output-channel-p1 channel type state)
           (b* (((mv & & state)
                 (read-object other-channel state)))
             (open-output-channel-p1 channel type state))))

Theorem: open-output-channel-p1-under-princ$

(defthm open-output-channel-p1-under-princ$
  (implies (open-output-channel-p1 channel type state)
           (b* ((state (princ$ x other-channel state)))
             (open-output-channel-p1 channel type state))))

Theorem: open-output-channel-p1-under-write-byte$

(defthm open-output-channel-p1-under-write-byte$
  (implies (open-output-channel-p1 channel type state)
           (b* ((state (write-byte$ byte other-channel state)))
             (open-output-channel-p1 channel type state))))

Theorem: open-output-channel-p1-under-print-object$

(defthm open-output-channel-p1-under-print-object$
  (implies (open-output-channel-p1 channel type state)
           (b* ((state (print-object$ byte other-channel state)))
             (open-output-channel-p1 channel type state))))

Theorem: open-output-channel-p1-under-set-serialize-character

(defthm open-output-channel-p1-under-set-serialize-character
  (implies (open-output-channel-p1 channel type state)
           (b* ((state (set-serialize-character c state)))
             (open-output-channel-p1 channel type state))))