search

ClemsonRSRG / RESOLVE

RESOLVE (REusable SOftware Language with VErification) is a specification and programming language designed for verifying correctness of object oriented programs.
https://www.cs.clemson.edu/resolve/
BSD 3-Clause "New" or "Revised" License
24 stars 16 forks source link

Don't add 'false' as an antecedent and 'true' as an succedent if they… #391

Closed yushan87 closed 2 years ago

yushan87 commented 2 years ago

Don't add false as an antecedent and true as a succedent if they are by themselves in the sequent.

Below is an explanation by Bill Ogden.

One conclusion I'm drawing from today's meeting is that the VC sequent generator should be eliminating ALL the Boolean operators in favor of a sequent form involving only the functions, predicates, and constants from the math theories used to formulate the specs in the code being verified. This means also eliminating the Boolean constants True and False. For the implicit and operator in an antecedent, True is an identity element (i. e., ( F1 and F2 and ... and Fn and True ) = ( F1 and F2 and ... and Fn ) ) and False is a zero element (i. e., ( F1 and F2 and ... and Fn and False ) = ( False ) ). Dually, for the implicit or operator in a succedent, False is an identity element (i. e., ( F1 or F2 or ... or Fn or False ) = ( F1 or F2 or ... or Fn ) ) and True is a zero element (i. e., ( F1 or F2 or ... or Fn or True ) = ( True ) ).

In the zero element cases, the Boolean constant can be eliminated by expressing: A ==> { True } by A ==> { } and { False } ==> S by { } ==> S.

When displaying the VCs for users, you probably want to leave the zero element cases with the Boolean constant left in the succedent or antecedent, but the sequent elaborator will be cleaner with the Boolean constants eliminated.