Added extra use-case hints to the already present invariant definitions.

Author: NlightNFotis

src/util/invariant.h

@@ -225,15 +225,26 @@ inline void invariant_violated_string(
 // for INVARIANT.
 
 // The condition should only contain (unmodified) arguments to the method.
+// Inputs include arguments passed to the function, as well as member
+// variables that the function may read.
 // "The design of the system means that the arguments to this method
 //  will always meet this condition".
+//
+// It is also supposed to signal that even though an object is in a
+// valid state, a particular function may not be operating on objects
+// with the particular properties this one has.
 #define PRECONDITION(CONDITION) INVARIANT(CONDITION, "Precondition")
 #define PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
   INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
 
 // The condition should only contain variables that will be returned /
 // output without further modification.
 // "The implementation of this method means that the condition will hold".
+//
+// A POSTCONDITION documents what the function can guarantee about its
+// output when it returns, given that it was called with valid inputs.
+// Outputs include the return value of the function, as well as member
+// variables that the function may write.
 #define POSTCONDITION(CONDITION) INVARIANT(CONDITION, "Postcondition")
 #define POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
   INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
@@ -242,6 +253,10 @@ inline void invariant_violated_string(
 // changed by a previous method call.
 // "The contract of the previous method call means the following
 //  condition holds".
+//
+// A difference between CHECK_RETURN and POSTCONDITION is that CHECK_RETURN is
+// a statement about what the caller expects from a function, whereas a
+// POSTCONDITION is a statement about guarantees made by the function itself.
 #define CHECK_RETURN(CONDITION) INVARIANT(CONDITION, "Check return value")
 #define CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...)  \
   INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
@@ -254,14 +269,18 @@ inline void invariant_violated_string(
 // This condition should be used to document that assumptions that are
 // made on goto_functions, goto_programs, exprts, etc. being well formed.
 // "The data structure is corrupt or malformed"
+//
+// It is okay for a DATA_INVARIANT to have an empty string as a reason string
+// if you can't state the reason, or doing so doesn't add any information -
+// just restates the condition.
 #define DATA_INVARIANT(CONDITION, REASON) INVARIANT(CONDITION, REASON)
 #define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
   INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
 
 // Legacy annotations
 
 // The following should not be used in new code and are only intended
-// to migrate documentation and "error handling" in older code
+// to migrate documentation and "error handling" in older code.
 #define TODO           INVARIANT(false, "Todo")
 #define UNIMPLEMENTED  INVARIANT(false, "Unimplemented")
 #define UNHANDLED_CASE INVARIANT(false, "Unhandled case")