CPSC 2150 - DAY 15
OCTOBER 18, 2016

================================================================================

REASONING BASICS
----------------

Quality assurance Techniques

	.Testing
	.Tracing (or inspection)
	.Formal reasoning 

Use a verifier (like a compiler) on the code
Analyze, but not execute code
Show logical errors, when proof fails

#this is the stack before pop
this is the stack after pop

Reasoning about correctness
	.Show that the code does what its contract says it must do.
	.Show that the code does not violate any contracts on which it depends

Reasoning
	.Assume M's requires clause
	.M's code	
	.Confirm M's ensures clause

Formal Reasioning: top Method

	.Show that the code does what its contract says it must do
		.Show that any implicit insures clause holds (ie this = #this)
		.Show that the ensures clause holds at the end of the code

	.Show that the code does not violate any contracts on which it depends

	.Show thad the code does not violate any contracts on which it depends
		.call for pop does not violate pop's requires clause
		.call for pop does not violate push's requires clause