frama-c - frama-c / ACSL / WP : セットのカーディナリティ

Question

他の正式な仕様でセットのカーディナリティをよく使用しますが、WP frama-c プラグインを使用して ACSL で使用できるかどうか疑問に思っています。

たとえば、書く assumes card({*a, *b, *c}) == 3 よりも 書く方が明確に思えます。assumes *a != *b && *a != *c && *b != *c