[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: pvs-help@csl.sri.com*Subject*: Accumulation quantifier support?*From*: Bill McUmber <bill@spi.org>*Date*: Tue, 30 Sep 1997 11:27:20 -0400 (EDT)

What sort of support exists and how would one go about writing so-called accumulation quantifiers such as found in Gries/Schneider book, Chap 8 (as well as elsewhere). In general, terms like (*i: R(i): P(i)) where the operator * is applied to each P(i) over the range specified by R(i). The operator for FORALL is conjunction, EXISTS, disjunction, etc. The primary one needed is the 'Count of' (Gries 'N' operator): (Ni: R(i): P(i)) gives the count of P(i) true in the range. In the static case, this can be written as a rather large disjunction but in the variable case I don't think it can. Thanx much. Bill McUmber bill@spi.org or mcumber@cps.msu.edu

- Prev by Date:
**WITH and dependent types** - Next by Date:
**Re: Accumulation quantifier support?** - Prev by thread:
**Union over a set; quantifiers** - Next by thread:
**Re: Accumulation quantifier support?** - Index(es):