Reasoning about ACL2 file input

We introduce the logical story behind file input in ACL2 and discuss the types of theorems that can be proven about filereading operations. We develop a low level library for reasoning about the primitive input routines. We then develop a representation for Unicode text, and implement efficient functions to translate our representation to and from the UTF-8 encoding scheme. We introduce an efficient function to read UTF-8-encoded files, and prove that when files are well formed, the function produces valid Unicode text which corresponds to the contents of the file. We find exhaustive testing to be a useful technique for proving many theorems in this work. We show how ACL2 can be directed to prove a theorem by exhaustive testing. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification—correctness proofs, formal methods; D.2.1 [Software Engineering]: Requirements/Specifications General Terms Verification, Performance Keywords ACL2, file...

• Type: Conference
• Year: 2006
• Where: ACL2
• Authors: Jared Davis
• Keywords: ACL2 2006, Computational Linguistics, Exhaustive Testing, Unicode Text, file Input