Week 1

Introduction

To verify code, a method was needed to find the system worked well or not.

Hoare introduced Hoare triple model： {P} Precondition S {Q} Postcondition After procedure S , the system entered Q, then the triple is True, otherwise False.

Dijkstra improvement

Worst precondition

Repetition: {R} do B -> S od

"establish P" {P} do B -> {P $\wedge$ bB and }