This is a an example lecture from a course on Formal Methods for Computer Science on the topic of program verification. In this webinar I prove a simple property of two programs over lists (length and append) by induction over lists.
In addition to illustrating issues in program verification, the webinar demonstrates the use of an induction principle unfamilar to many: list induction. Most people with a little mathematical training know about numerical induction. What is less well known is that induction principles can be derived for any well-ordered set -- in this case that set comprises all lists; and the ordering is the transitive closure of the immediate tail-list ordering.
Testing at present ...
