Proposal for clarifying the meaning of "forall"

Hi all,

I am re-sending the proposal for clarifying the meaning of "forall", with a
few updates. The original email was sent on Dec. 12, 2004.

I believe that similar clarifications should be included in the section on
"for". Most of them already exist in Dana's proposal, I think the only
necessary additions are notes such as (I.a) and (I.d) below.

Changes for clarifying the meaning of forall
------------------------------------------------

(I) Section 6.2.3 Replicated properties

(I.a) Add the following note after Box 78 (page 79)
"Note: the term "/replicated/ /property/" is used figuratively. It does not
imply that replication actually takes place. Whether or not any part of the
property is replicated depends on the implementation".

(I.b) Change the paragraph on page 79, lines 53-55, to the following:
"1) If the parameter is not an array, then the property is equivalent to a
property obtained by the following steps:
(i) replicating the parameterized property for each value in the set of
values, with that value substituted for the parameter (so that the total
number of replications is equal to the size of the set of values)
(ii) logically "anding" all of the replications."

(I.c) Change the paragraph on page 80, lines 1-4, to the following:
"2) If the parameter is an array of size N, then the property is equivalent
to a property obtained by the following steps:
(i) replicating the parameterized property for each possible combination of
N (not necessarily distinct) values from the set of values, with those
values substituted for the N elements of the array parameter (if the set of
values has size K, then the total number of replications is equal to K^N)
(ii) logically "anding" all of the replications."

(I.d) Add the following paragraph after the preceding paragraph (page 80,
line 5):
"Note that in both cases the meaning of a replicated property is
/equivalent/ to the replication process. This does not imply that any
replication must actually take place."

(I.e) Change the note on page 80, lines 37-38, to the following:
"Note— The parameter defined by a replicator is considered to be statically
computable..."

(I.f) Add another note on page 80, line 39 (after the existing note)
"Note- parameterized properties (Section ???) are a generalization of the
forall construct. Any property written with forall can be written
equivalently using a parameterized logical and operator. The forall
construct is currently maintained in the language for reasons of backward
compatibility.

(I.g) Replace the Informal Semantics section (starting on page 80, line 40)
with the following:

—A forall i in boolean: f(i) property is equivalent to:
f(true) && f(false)

—A forall i in {j:k} : f(i) property is equivalent to:
f(j) && f(j+1) && f(j+2) && ... && f(k)

—A forall i in {j,l} : f(i) property is equivalent to:
f(j) && f(l)

—A forall i[0:1] in boolean : f(i) property is equivalent to:
f({false,false}) && f({false,true}) && f({true,false}) && f({true,true})

—A forall i[0:2] in {4,5} : f(i) property is equivalent to:
f({4,4,4}) && f({4,4,5}) && f({4,5,4}) && f({4,5,5})
      && f({5,4,4}) && f({5,4,5}) && f({5,5,4}) && f({5,5,5})

(I.h) The second "Illegal" example should be moved to the "Legal" examples
section (page 81 lines 49-51).

_______________________________________________________
Avigail Orni
Verification and Testing Solutions Group
IBM Haifa Research Laboratory
Phone: 972-4-829-6396 email: ornia@il.ibm.com
Received on Fri Jan 21 02:31:26 2005