Последовательные и параллельные утверждения
Мысль о том, что утверждения, в частности предусловия, могут иметь две разные семантики - условий корректности и условий ожидания, может показаться странной. Но без этого не обойтись: последовательная семантика не применима в случае сепаратных предусловий.
Нужно ответить на одно возможное возражение. Мы видели, что проверку утверждения во время выполнения можно включать или отключать. Не опасно ли тогда придавать так много семантической важности предусловиям в параллельных ОО-системах? Нет. Утверждения являются неотъемлемой частью ПО независимо от того, проверяются ли они во время исполнения. В последовательной системе корректность означает, что утверждения всегда выполняются, поэтому из соображений эффективности можно отключить их проверку, если есть уверенность в том, что ошибок не осталось, хотя концептуально утверждения все еще присутствуют. В параллельном случае отличие состоит в том, что некоторые утверждения - предложения сепаратных предусловий - могут нарушаться во время выполнения даже в корректной системе и должны служить условиями ожидания.
