SpeAR should support sets and first-order quantifiers

[manthonyaiello]

Increasingly, we want to be able to state properties about sets that involve the use of first-order quantifiers. This has come up in the UCP but particularly in the work being done on UxAS.

Since I understand the complexity of this proposition, especially given some of the restrictions in Lustre, I propose the following road map to build up to sets and first-order quantifiers:

1. Build a model/reference bounded-size set datatype. For example:

   set_element_type is an int
   set_storage_type is a set_element_type[3]
   set_type is a record {
     cardinality: int,
     storage: set_storage_type
   }

   This set is of bounded size 3.

2. Build a model/reference bounded-size set abstraction, using patterns. For example, we might include:

   • empty: returns true if the set is empty
   • full: returns true if the set is full
   • cardinality/size: returns the number of elements in the set
   • includes/contains: returns true if the set contains the given element
   • insert:
     • if the set is full, returns the set;
     • if the set contains the given element, returns the set;
     • returns the set, modified such that the set now contains the given element
   • delete:
     • if the set is empty, returns the set;
     • if the set does not contain the given element, returns the set;
     • returns the set, modified such that the set no longer contains the given element
   • select/choose:
     • returns an item from the set, at random
     • challenge: what should this do, if the set is empty? perhaps a property to prove is that choose is not called on an empty set

3. Build a model/reference collection of properties for the use of sets. We'd keep adding to this as we enhanced/expanded the set/quantifier support.

4. Modify SpeAR so that patterns can take predicates as arguments. Having predicates as arguments to patterns would enable us to build up quantifiers for bounded-size set abstractions manually, using patterns. We could then define patterns:

   • exists: returns true if the given predicate holds for any element in the set
   • all: returns true if the given predicate holds for all elements in the set

   These predicates could follow a pre-defined syntax and could even be introduced with a special keyword, as needed. The syntax would ensure/provide that the first argument to the predicate is an element of the set, for instance:

   pattern predicate(element: set_element_type, [...]) returns (result: bool)

   I'm guessing that Lustre will not permit this directly, so we'd have to do some heavy work in the code generator to handle the composition of functions this would imply.

5. Modify SpeAR so that patterns and datatypes can be genericized (à la Java). We can put appropriate/reasonable restrictions on this, I hope, so that we don't run into huge problems. Since SpeAR doesn't have data-type inheritance, I think a lot of the complexity in Java generics would drop away, but I've not thought about this very hard.

   If generics are a no-go, then having some sort of support in SpeAR to generate a set type and pattern library would be really nice. It'd basically just be template instantiation, and so shouldn't be terribly hard to do. We could of course accomplish much the same with appropriate regex find-replace, but having something build into the tool/language would be really nice.

6. Modify SpeAR to "internalize" the patterns and properties for the set abstraction. That is, rather than having SpeAR text for the patterns in a types file and rather than having properties manually included in the spec files, the tool would include that support in an internal library that the user would never see. This actually might be a good way to get around item (5) above - although we'd still need some way for the user to actually reference the instantiated generic type. (I need to be able to talk about my set of bananas in my spec.)

7. Modify SpeAR so that it can automatically adjust the size of the set. For example, through the preferences dialog, we could say that the minimum size of the set was 3 and the maximum size of the set is 5. SpeAR would then prove our properties for 3, 4, and 5 as the maximum size of the set. (Or possibly just for 3 and 5.)

   The thought here is that by setting a min and a max, you get some early feedback (I proved your properties for a small number of allowed elements) before the system tried the proofs on larger sets. My guess is that, for requirements, only a small number of elements in the set at a given time would be required to show problems.

In parallel with all of the above, we'd research approaches to quantification over arbitrary/infinite sets in bounded model checking. My guess is that this would be very hard, which is why I recommend the build-up approach that's shown above.

Regardless, we should get some interesting papers out of any work we do on this.

[manthonyaiello]

Attached is a candidate reference implementation of the set datatype and the basic (non-quantifier) patterns, based on work I'd already undertaken for UxAS. This is close to generic, because of the use of a custom element type and a constant for the default element.

I should note that this has not been tested in any way and also that choose doesn't work because I don't know how to build a random pattern.

set.spear.txt

[lgwagner]

Tony I provided partial support for this in 2.1.0. I have serious concerns that if we add all of these features you're asking for that we won't be able to scale up to sets of any appreciable size.

We should sit down and hand modify some SpeAR examples, if and when it is appropriate. I'll leave this particular issue open for a while.