Introduction to Verification

OVERVIEW



WHAT IS VERIFICATION?

Verification is demonstration that implementation "agrees" with a specification

Specifiction:

PROOF

LOGIC as a Specification Notation

PROGRAM STATES

SPECS and PROGRAM EXECUTION


A GENERIC EXAMPLE: REASONING ABOUT PROGRAM STATES

Consider this algorithm and environment...
   INITIAL STATE:
      a can of beans, G and R
      a pile of extra G beans (more than enough)
  
   ALGORITHM:
      while possible 
         draw out two beans
         if both G or both R 
            discard both
            return a G to the can
         if one G and one R
            put the R back in the can
      end

SEMI-FORMAL ARGUMENT

Questions:

There are two issues in program verification...

Together, these two are 'total correctness'

SEMI-FORMAL REASONING

INFERENCE SYSTEMS

HOARE'S AXIOMATIC METHOD

We will see in the notes on the Axiomatic Method of program verification will use an extended inference system: