Specifications Partial correctness: ip}eta} Total correctness: [p]c[a] Note the spec now requires c does not abort. Specifications Partial correctness: Total correctness: Note the spec now requires c does not abort