Never Claim とは (what is never claim?)

In formal methods in software engineering, "a never claim" represents a property of the system that should never be satisfied during the execution of a model/system.

Never claim is considered to be useful notion. Since it is easier to prove that a model does not satisfy a property than it is to prove that it does, i.e. it only takes one counter-example to shown that a property is not satisfied. A never claim is therefore typically used to represent the negation of the formula (property) of interest. To prove F, a never claim is generated for !F – the negation of F. SPIN then checks the model against !F:

• If an acceptance cycle is detected then !F is satisfied and

a counter-example exists for F.

• If no acceptance cycle is detected then !F is not satisfied,

and therefore F is satisfied by the model.

bib: http://www.macs.hw.ac.uk/~air/dsp-spin/lectures/lec-8-how-it-works.pdf