AFFIRM

Paul McJones, editor
paul@mcjones.org
https://mcjones.org/dustydecks/

Last modified 19 January 2011

AFFIRM was a program verification system developed at USC Information Sciences Institute.

"AFFIRM is an experimental interactive system for the specification and verification of abstract data types and programs. It was developed by the Program Verification Project at the USC Information Sciences Institute (lSI) for the Defense Advanced Research Projects Agency.

...

The USC/Information Sciences Institute Program Verification Project is headed by Susan L. Gerhart, with members Roddy W. Erickson, Stanley Lee, Lisa Moses, and David H. Thompson. Past proje('( members include Raymond L. Bates, Ralph L. London, David R. Musser, David G. Taylor, and David S. Wile." [Thompson and Erickson 1981]

Source code

Index.pdf

• AffirmExec.pdf
• Boolean.pdf
• Build.pdf
• CEval.pdf
• FormulaIO.pdf
• Handcoded.pdf
• Help.pdf
• InfixPrint.pdf
• Init.Lisp.pdf
• Integer.pdf
• LibProc.pdf
• Limbo.pdf
• Logic.pdf
• Miscellaneous.pdf
• Parser.pdf
• ParserHelper.pdf
• ParserPlus.pdf
• Pascal.pdf
• ProcedureCall.pdf
• Profile.pdf
• ProofStructure.pdf
• Request.pdf
• RewriteRule.pdf
• Specification.pdf
• Sufficient.pdf
• TEdit.pdf
• TheoremProver.pdf
• Tree.pdf
• Utility.pdf
• VCGen.pdf
• XEval.pdf

Documentation

• David H. Thompson and Roddy W. Erickson, editors. AFFIRM Reference Manual. Version 2.0 (AFFIRM Version 1.21), USC Information Sciences Institute, February 19, 1981. PDF
• Susan L. Gerhart, editor. AFFIRM Type Library. Version 2.0 (AFFIRM Version 1.21), USC Information Sciences Institute, February 19, 1981. PDF
• Raymond L. Bates and Susan L. Gerhart, editors. AFFIRM Annotated Transcripts. Version 2.0 (AFFIRM Version 1.21), USC Information Sciences Institute, February 19, 1981. PDF
• Roddy W. Erickson, editor. AFFIRM Collected Papers [bibliography only]. Version 2.0 (AFFIRM Version 1.21), USC Information Sciences Institute, February 19, 1981. PDF
• David H. Thompson, editor. AFFIRM Demo Handbook. Version 2.0 (AFFIRM Version 1.21), USC Information Sciences Institute, May 8, 1981. PDF