Added pre and pos conditions to procs.
Starting on iterative assertion verification.