A partial correctness claim connecting a precondition , a program and a postcondition : every terminating execution begun with ends with . State separately whether total correctness is intended.
New to topics? Read the docs here!
New to topics? Read the docs here!