I. Introduction A. terminology random numbers in Haskell? B. goals and techniques ------------------------------------------ FUNCTIONAL PROGRAMMING GOALS AND TECHNIQUES Goals: Programming Techniques: ------------------------------------------ 1. the Von Neumann Bottleneck (Davie 1.1, 1.3) (omit) ------------------------------------------ THE VON NEUMANN BOTTLENECK !---------! !-----------! ! ! ! ! ! CPU ================= Memory ! ! ! ! (RAM) ! !---------! ! ! !-----------! ------------------------------------------ what's the purpose of a program? How is this reflected in programming languages? what helps aleviate this? C. interest and applications (omit most of this) 1. programming 2. reuse 3. language design 4. semantics 5. types 6. reasoning D. History (omit) II. reasoning in functional languages contrasted with imperative languages (omit) How do you specify and verify imperative programs? ------------------------------------------ SPECIFICATION AND VERIFICATION FOR IMPERATIVE PROGRAMS // Larch/C++ behavioral specification //@ uses FactorialTrait; void factAssign(int & x, int n); //@ behavior { //@ requires n >= 0; //@ modifies x; //@ ensures liberally x' = factorial(n); //@ } % Vocabulary definition in LSL FactorialTrait: trait assumes int introduces factorial: int -> int asserts \forall i: int factorial(0) == 1; (i >= 0) => (factorial(i+1) = (i+1) * factorial(i)); ------------------------------------------ ------------------------------------------ // CODE in C++ with VERIFICATION void factAssign(int & x, int n) { // ASSERT: n >= 0 int i = 0; x = 1; // INV: n >= 0 /\ x = factorial(i) // /\ i <= n while (i < n) { i++; // ASSERT: n >= 0 // /\ x = factorial(i-1) // /\ i-1 <= n x *= i; } // ASSERT: x = factorial(i) /\ i = n // hence // ASSERT: x = factorial(n) } ------------------------------------------ Can the i++ come after the x *= i? Is it in the right order? why? Is the test in the while loop exactly right? ------------------------------------------ SPECIFICATION AND VERIFICATION FOR FUNCTIONAL PROGRAMMING -- "Larch/Haskell" behavioral spec. uses FactorialTrait(Integer for int) -- the trait is the same as before fact :: Integer -> Integer fact(j) | j >= 0 = factorial(j) -- implementation in Haskell fact(n) = factIter(n,1) fact :: (Integer,Integer) -> Integer factIter(0, i) = i factIter(n+1, i) = factIter(n, (n+1)*i) ------------------------------------------ ------------------------------------------ VERIFICATION USING EQUATIONAL REASONING Theorem: if j > 0, fact(j) = factorial(j) Proof: fact(j) = factIter(j,1) = factorial(j)*1 Lemma: For all i >= 0, factIter(i,k) = factorial(i)*k Proof: Basis: j = 0 factIter(0,k) = { definition } k = { arithmetic } 1 * k = { specification } factorial(0) * k Inductive step: j = n+1 Ind Hyp: factIter(n,k) = factorial(n)*k factIter(n+1, k) = { definition } factIter(n, (n+1)*k) = { Ind Hyp} factorial(n)*(n+1)*k = { definition of factorial } factorial(n+1)*k ------------------------------------------ How would you compare the two proofs? Which uses simpler math? Which would be easier to teach? Which would you be more confident in? ------------------------------------------ VERIFICATION PROBLEMS WITH IMPERATIVE LANGUAGES Aliasing: two names for the same variable Is this valid for C++? // ASSERT: x = 4 /\ y = 4 x = 7; // ASSERT: x = 7 /\ y = 4 Not referentially transparent: an expression changes meaning over time Is this valid for C++? b = (f() == f()) // ASSERT: b = true Others: - ------------------------------------------ What other problems (bugs) are typical in imperative languages?