Comparing Proofs about I/O in Three Programming Paradigms
Andrew J. Butterfield, Glenn Strong · 2002
Syntaxes 13 3.1 Common Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 3.1.1 Common Expressions . . . . . . . . . . . . . . . . . . . . 13 3.1.2 Functional Language Expressions . . . . . . . . . . . . . . 13 3.2 C Abstract Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . 14 3.2.1 C Statements . . . . . . . . . . . . . . . . . . . . . . . . . 14 3.2.2 C Programs . . . . . . . . . . . . . . . . . . . . . . . . . . 14 3.3 Clean Abstract Syntax . . . . . . . . . . . . . . . . . . . . . . . . 14 3.3.1 Clean Expressions . . . . . . . . . . . . . . . . . . . . . . 14 3.3.2 Clean Hash Elements . . . . . . . . . . . . . . . . . . . . 14 3.3.3 Clean Programs . . . . . . . . . . . . . . . . . . . . . . . 14 3.4 Haskell Abstract Syntax . . . . . . . . . . . . . . . . . . . . . . . 15 3.4.1 Haskell Expressions . . . . . . . . . . . . . . . . . . . . . 15 3.4.2 Haskell Monadic Statements . . . . . . . . . . . . . . . . . 15 3.4.3 Haskell Programs . . . . . . . . . . . . . . . . . . . . . . . 15 1 4 Real Programs 15 4.1 The real C program . . . . . . . . . . . . . . . . . . . . . . . . . 15 4.2 The real Clean program . . . . . . . . . . . . . . . . . . . . . . . 16 4.3 The real Haskell program . . . . . . . . . . . . . . . . . . . . . . 16 5 Abstracted Programs 16 5.1 The IO abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . 17 5.2 Concrete Programs using IO Abstraction . . . . . . . . . . . . . 17 5.2.1 The abstracted C program . . . . . . . . . . . . . . . . . 17 5.2.2 The abstracted Clean program . . . . . . . . . . . . . . . 17 5.2.3 The abstracted Haskell program . . . . . . . . . . . . . . 18 5.3 Abstract Syntax Forms . . . . . . . . . . . . . . . . . . . . . . . . 18 5.3.1 Abstract Syntax for C Program . . . . . . . . . . . . . . . 1...