enter image description here

Im trying to make an invariant for this Z schema about routes.

1) The invariant should express that each route should contain at least 20 different places. First of all i thought of doing a universal quantification such as:

∀x : ran routes • ( #x>20 ∧ x ≠ x')

However i'm really not sure if thats correct that implying 20 different places.


If you say

$\forall x, x': ran\ routes . x<>x'$

You're only saying that the sequences are different. For example

$<London, Berlin, Paris>$ would be different to $<London, Paris, Berlin>$

Instead, you need two quantifiers

$\forall x: ran\ routes . \#x>20$


$\forall p,p': Place • p \in ran\ (ran\ routes) \land p' \in ran\ (ran\ routes) \implies p<>p'$

One for the length as you had and one for the condition that all elements must be unique. Note the double $ran$ expression since a sequence is defined as a function between its indexes and its values (the range).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.