Re: Proposal for clarifying the meaning of "forall"

All,

> 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.

I suggest to add the following notes to the sections on replicated
sequences and replicated properties, respectively.

Note: the definition given here is not bound to a specific
implementation. In particular, in many cases it is possible to
implement a parameterized sequence without replicating the base
compound SERE.

Note: the definition given here is not bound to a specific
implementation. In particular, in many cases it is possible to
implement a parameterized property without replicating the base FL
property.

Regards,
Dana.

On Fri, 21 Jan 2005 12:35:16 +0200, Avigail Orni <ORNIA@il.ibm.com> wrote:
>
>
> 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 Sun Jan 23 01:46:10 2005