Facts vs assertions?

Breaking this into a new topic… I’ve been advised to convert a fact to an assert. To me, the advantage of a fact is that it’s always applied, whereas I have to check an assertion explicitly. The Book talks about using assertions, either to express “mundane” properties (which begs the question about what is interesting in a model), or to express “essential properties.”

Clearly this is an area for heuristics, partly guided by the experience of interacting with the visualiser.

Any guidance?

Thx

I rarely use facts anymore after I also struggled with them. The key problem is that they exclude any instance that would have those facts.

When you make a model like your credit card model, you want to make sure that the sequence of steps, like cancel, can never reach an invalid state. If you use a fact, then those states are impossible to reach by definition. So your steps might only show nice instances but when you translate those ‘verified’ steps to code, you run into cases that you never verified because the ‘facts’ excluded that state space.

For example, you could make it a fact that each card in cards is issued:

     fact { Customer.cards.status in issued }

However, if your steps are broken then these broken steps are excluded from verification because the fact excludes them. However, your code likely won’t.

I use facts as assumed invariants of the environment and never use them to force my model to stay in the safe lane.

The purpose of an assert is to ensure that your steps cannot reach those invalid states. I.e. verify that every card in cards is always issued.

Hope this helps.

2 Likes

That’s a very helpful distinction (to me, at least).

Hi,

I guess it depends on the goal you intend to achieve with your model.

In the cards example, if your goal was to design the card operations such that they respect the card lifecycle, then the card lifecycle should not be a fact (which btw would make it necessarily true) but an assertion that is checked to hold.

If your goal was to write a model just to generate some valid scenario traces (for unit testing or eliciting requirements with your clients, for example), then you might even not model your operations, but use facts to characterise what is a valid execution scenario. This can even lead to simpler models. For example, one could write the following model to characterise valid scenarios in your example: in this case it is not exactly equivalent to your model (it allows more scenarios, for example a client getting a new card without replacing an existing one), but it is very simple and could be a good first approach to understand your problem.

open util/ordering[Status]

enum Status { unissued, issued, cancelled }

abstract sig Card {
	var status : one Status
}
sig DebitCard, CreditCard extends Card {}

sig Customer {
	var cards: set Card,
 	var debitCard: DebitCard
} {
	debitCard in cards
}

fact cards_issued_to_customers {
	always all disj c1, c2: Customer | no (c1.cards & c2.cards)
  	always Customer.cards = status.issued
}

fact card_lifecycle {
	always all card : Card | card.status' = card.status or card.status' = card.status.next
}

fact at_most_one_client_changes_cards {
	always lone c : Customer | c.cards' != c.cards
}

run {}

You could even start by doing a model like the latter and then move on to design operations such that the requirements (now in assertions) hold.

Best,
Alcino

Thanks all. So, if I don’t look too closely, I could compare facts/assertions to pre/post conditions?

  • pre = this must be true for the rest of the discussion to make sense
  • post = this is what we want to achieve

Aren’t facts invariants? Which would make them implicitly both pre- and post-conditions.

True. I did say not to look too carefully. I was thinking about an analogy to help us poor procedural coders make the transition.

Alternative, the initial state of the traces becomes the pre-conditions.

I would not use those terms in the context of a model. A model is a set of constraints on a universe, it does not really matter if you use facts, predicates, or any of the other ways to specify constraints on the model, they are basically the same after parsing. Pre and post imply a transition that might be part of your model, like in an event modelling method, but which does not sound helpful to me on the level of a model.

The only difference between predicates and facts is that the facts are always on, they are global for your model, while predicates need to be reachable from the run or check command to act as a constraint on your model.

Some comments about facts and invariants:

  • the term invariant is subject to various meanings depending on situations:
    • it may refer, in the style of so-called axiomatic semantics or Floyd-Hoare assertions, to a property that is preserved by every operation. Which requires, in your model, a notion of operation or event or action… You may check these properties with pure Alloy in fact.
    • in some contexts, people use the term to refer to properties that are always true, that is true in every reachable state. In Electrum, this would correspond to a property of the shape always P, P being a pure first-order constraint.
  • general facts are axioms: that is constraints imposed on any instance. They may contain any constraint: therefore they are not necessarily invariants.
  • signature facts are implicitly preprended an always connective so, if they only contain a pure first-order constraint, then they define an invariant (this is to mimick class invariants of OO design).

About events: for typical modelling, I would advise to use predicates to represent events. Using sigs is risky: indeed, in some contexts, due to the command scope applying to event sigs too, you may prune instances which require more events than there are possible instances for them, and (possibly) miss the violation of a property. Predicates are OTOH immune to this. If you still want to visualize events and manipulate them like sigs, I think it’s better to use event reification.

Thanks for this. I just showed a version to colleagues and they liked the idea of reifying the action in some way so that it’s easy to see how a step was triggered. I’ll take a look at your link.

I generally don’t like using asserts at all, since they’re a holdover from the time that check couldn’t take predicates. I find it easier to just write the assert as a pred and then check it.

1 Like

Steve Freeman via The Alloy Language and Tools
alloytools@discoursemail.com writes:

Breaking this into a new topic… I’ve been advised to convert a fact
to an assert. To me, the advantage of a fact is that it’s always
applied, whereas I have to check an assertion explicitly. The Book
talks about using assertions, either to express “mundane” properties
(which begs the question about what is interesting in a model), or to
express “essential properties.”

Interesting discussion! I started with Alloy recently.
My experiences with this so far:
I am tending to use facts mostly when creating “static” models
(no time related component and no operations).
When creating a model with operations, most of the facts can be
converted to assertions because of the structure of the
operations.
The trick mentioned by Hillel Wayne that one can check
predicates as well sounds very interesting. I will try this out
next.