I. Introduction
 A. overview
------------------------------------------
         FUNCTIONAL PROGRAMMING

Shorthand for:




Interest:








------------------------------------------
 B. the problem
  1. the Von Neumann Bottleneck (Davie 1.1, 1.3)
------------------------------------------
      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?
  2. reasoning with side effects, aliases, etc. (Davie 1.2)
	How are bridges engineered?
	If we were to "engineer computations" what would that be like?
	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?
 C. goals and techniques
------------------------------------------
	FUNCTIONAL PROGRAMMING
	 GOALS AND TECHNIQUES

Goals:





Programming Techniques:








------------------------------------------
 D. Semantic characteristics of Applicative languages
------------------------------------------
         SEMANTIC CHARACTERISTICS
         OF APPLICATIVE LANGUAGES

+ no storage cells, only values

    immutable lists:






    mutable lists:






+ no assignment, only binding






------------------------------------------