Representing conditional statements in Alloy Analyzer

Question

I am trying to represent conditional (if-else) statements using alloy. My understanding is that I need to use Hoare triples. However, I don't have much experience with software verification tools and I can't find any online tutorials that demonstrate it.

Answer 1

The basic syntax for conditional statements is implies:

 cond => expr [ else expr ]

You can also use:

 cond implies expr [ else expr ]

However, make sure you understand the logical rules for implies/=>.

This sounds rather a fundamental program; did you read Daniel Jackson's book? Did you look at simple examples, for example in the model repo?