Elaborate please; Without reasoning about programs how do you come up with the predicates which constitute a Model? Are you making a distinction between declara

Elaborate please; Without reasoning about programs how do you come up with the predicates which constitute a Model? Are you making a distinction between declarative logic used in specifications vs. say predicate transformers used in proving program correctness?