CIS 301. Program Verification

• The program Copy1:

    a = x;
    y = 0;
    while (a != 0) {
       y = y + 1;
       a = a - 1;
    }
  

• The program Mult1:

      a = 0;
      z = 0;
      while (a != y) {
        z = z + x;
        a = a + 1;
        }
  

• The program Mult2:

    z = 0;
    while (y != 0) {
      z = z + x;
      y = y - 1;
      }
  

• The program Fac1 for computing the factorial:

      y = 1;
      z = 0;
      while (z != x) {
        z = z + 1;
        y = y * z;
      }
  

• A program containing an If-statement:

      a = x + 1;
      if (a - 1 == 0) {
        y = 1;
      }
      else {
        y = a;
      }
  

• A program for computing the minimum of two values:

     if (x > y) {
       z = y;
     }
     else {
       z = x;
     }
  

• A program for multiplying two numbers: Multi1

      a = 0;
      z = 0; 
      while (a != y) {
        z = z + x;
        a = a + 1;
      }
  

• A downward version for computing the factorial: DOWNFAC

      a = x;
      y = 1;
      while (a > 0) {
        y = y * a;
        a = a - 1;
      }