CODEWITHSUNDEEP
alloy
John Wickerson
John Wickerson

Reputation: 1232

True and False in Alloy

Alloy has plenty of logical connectives like and and or and implies. But I can't find true and false. Are they missing? At the moment I've been making do with 1=1 and 1=0, but this is rather hacky (and gives a compiler warning).

My reason, by the way, for wanting true and false is that I'm writing something that produces an .als file. My top-level .als file expects that my auto-generated .als file defines a wellformed predicate and a faulty predicate. Sometimes these predicates are complicated, but sometimes I just want wellformed[...] to return true, and faulty[...] to return false. This is why I want true and false in the Alloy language.

Upvotes: 1

Views: 705

Answers (3)

Daniel Jackson
Daniel Jackson

Reputation: 2768

They're not built in for a good reason: see the FAQ on p137 of Software Abstractions (Daniel Jackson, MIT Press, 2012). The issue in short is that if they were built in, you'd have to be able to declare a relation over the booleans, and then because boolean expressions could evaluate to {} and {T,F}, the connectives would need to be defined over these values, and that seemed like a really bad idea.

Upvotes: 4

Alcino Cunha
Alcino Cunha

Reputation: 186

Since an empty predicate is true, my favorite implementation of true and false is:

pred true {}
pred false { not true }

Upvotes: 3

user1513683
user1513683

Reputation: 419

pred true {no none}
pred false {some none}

seems to work; but it would be nice to have these inbuilt.

Upvotes: 1

Related Questions