• Imperative programming
  • The variables can change their values as the program is running
  • programs that are written are not the same as the computations that take place during the execution
    • If we write a loop, computations will keep on going but we didn't enumerate all the computations
• Definition of structured programming on page 61
• Chapter 3 deals with
  • Different control structures used to write structured programs
  • Proof of the correctness of the given program segment
• Control structures
  • Conditional control structure
    • if and case/switch
  • Iterative Structures
    • while do/while
    • repeat until/do while
    • for
• If statement in Pascal
  • The problem of dangling else
  • Modula-2 uses and end to terminate the if statement
  • The association of else with the if in modula-2 is explicit
  • The modula-2 syntax may not be as concise as Pascal for several nested if's. Because every if has to have an end
  • This problem is overcome by using a special keyword called elsif. Syntax is on page 77 using EBNF.
  • Even though the programming language syntax tries to make sure that there no loopholes, we should try to not use complicated conditional statements. Too much of nesting is going to make the program unreadable.
• case/switch (page 70-71)
  • Syntax of switch in C

switch(expression)

{

case constant: <statements>

case constant: <statements>

.

.

.

default: <statements>

}

• In C the switch statement has a fall through effect.
• The cases should not be repeated - no duplicate cases. In C, the cases have to be constant so the compiler can catch the duplicate cases
• C provides default action, so does Modula-2 but not Pascal.
• The implementation of the case statements can be efficient, especially in case of large number of cases.
• Larger cases are handled by jump table or if the jump table is sparse, hash table is used (page 71-72)
  • For example, if the cases consist of numbers from 100 to 200, then create a table of 200-100+1=101 entries. For each value, there is an entry to tell where to go for that value. Works very well if almost all the values are represented in the case statement
  • If the values go from 100 to 100,000 and only 500 hundred of them appear in the case statement, we should use hash table (COSC 2007).
• Iterative statements
  • We really only need one type of iterative structure
  • Three different ones are provided to make the programs more readable
  • while loop may be executed zero times if the condition is false to start with.
  • do while checks the condition at the bottom. so the loop is executed at least once.
  • for loop combines three statements: initialization, checking the condition, reinitialization

for(i = 0; i < n; i++)

• In Pascal the for loop is more restrictive than C (surprize, surprize!)
• You can only use ordinals and you can either go up or down by one
• The expression in condition is evaluated only once.
• j = 10;
• for I := 0 to j do
• begin
• j = 25;
• end
• Just because the value of j was changed after entering the loop doesn't mean that the loop will be executed 26 times. It will be executed only 11 times.
• break, continue and return statements
• goto statements were considered a deterrent to the structured programming
• it is easy to write spaghetti like programs using goto statements
• Most languages still provide got statements. The use is discouraged. But responsible use of goto statements can actually improve the readability of the program
• break, continue, return are special type of goto's
• for(j = 0; j < n; j++)
• {
• if(.......) break; // gets you out of the loop
• if(......) continue; // takes you to the j++ at the top
• }
• int max(int i, int j)
• {
• if(i > j) return i;
• return j; // else is not needed
• }
• Generally, you should have clearly defined entry and exit points from a piece of code
• break, continue, and return take you to the entry or exit point.

• Proof of correctness using invariants and the proof rules
• Running example from page 61
• For the first statement after the while, x will always be the first element of a run. This is true irrespective of the value of x. That is why it is called invariant.
• Generally, for a logical piece of code such as a function, a loop or conditional structure we also use special invariants called precondition and postcondition
• Your code is going to assume that the precondition is true and going to gurantee that if the precondition is true then the postcondtion will be true.
• // k is not equal to zero
• int divisible(int j, int k)
• {
• if(j % k!=0) return 0;
• return 1;
• }
• //returns zero if j is not divisible by k and returns 1 otherwise
• Some more information on invariants on page 80
• Page 86. Proof rules: You prove smaller pieces of code and use proof rules to prove that the entire program is correct.
• Rule for statement composition (making use of transitivity)
• Rule for in condition: if you prove the top two things for S1 and S2, you have automatically proved the if statement
• Rule for while statement: if you prove the top statement for S, you have automatically proved the while statement
• How to prove an assignment statement
  • suppose you are looking for the postcondition Q
  • x = E
  • will gurantee that Q is true if Q[E/x] was the precondition. Q[E/x] is defined as replace all occurrences of x by E.
• Rule for simplification: If we have already proven that
• //P'
• S
• //Q'
• We have also proven
• //P
• S
• //Q
• as long as P =>P' and Q'=>Q
• The idea behind this technique is similar to math proofs
• Use previously know results and prove the new results
• If smaller building blocks of our program have been proven to be correct, then we can prove that the program is correct using the proof rules