> Peter Horan wrote:

James McKim wrote:

> > A fairly trivial observation, but worth a word.

> >

> > The postcondition of count is

> > consistent_with_bounds: Result = upper - lower + 1

> >

> > The postcondition of (for example) is_empty is

> > definition: Result = (count = 0)

> >

> > Other function postconditions are tagged "definition". Why not count?

> I agree, I prefer the word "definition" when we have one line that is

OK, there seems to be general agreement on this style guideline. At the

> defining a query.

end of this message I have shown how existing features of STRING and

ARRAY would look with their postcondition tags renamed.

> Ideally, though, each spec ought to carry a little road map so that it's

Although the group decided not to include this directed graph within the

> clear where a newcomer should start and progress to learn about the class.

> E.g.

>

> Basic queries: item, lower, upper

> 1st level derived queries: count, others?

> 2nd level derived queries: is_empty

>

> Actually a directed graph would be a better representation.

>

> I didn't win the argument to include this kind of thing, but I still

> think I'm right about this issue.

specification that forms the standard, it would still be interesting to

have within the explanatory material. So if anyone draws up the graph for

any ELKS class, feel free to post it here.

Here are the candidate versions of queries from classes ARRAY and STRING

where the result is fully-specified by a single postcondition and the tag

was not already "definition":

28 JANUARY 2002 VERSIONS (CLASS ARRAY):

count: INTEGER

-- Number of available indices

ensure

definition: Result = upper - lower + 1

(The tag was previously "consistent_with_bounds".)

28 JANUARY 2002 VERSIONS (CLASS STRING):

is_boolean: BOOLEAN

-- Does `Current' represent a BOOLEAN?

ensure

definition: Result = (same_string("true")

or same_string("false"))

(The tag was previously "is_boolean".)

is_double: BOOLEAN

-- Does `Current' represent a DOUBLE?

ensure

definition:

-- Result is true if and only if the following two

-- conditions are satisfied:

--

-- 1. In the following BNF grammar, the value of

-- `Current' can be produced by "Real_literal":

--

-- Real_literal = Mantissa [Exponent_part]

-- Exponent_part = "E" Exponent

-- | "e" Exponent

-- Exponent = Integer_literal

-- Mantissa = Decimal_literal

-- Decimal_literal = Integer_literal ["." Integer]

-- Integer_literal = [Sign] Integer

-- Sign = "+" | "-"

-- Integer = Digit | Digit Integer

-- Digit = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9"

--

-- 2. The numerical value represented by `Current'

-- is within the range that can be represented

-- by an instance of type DOUBLE.

(The tag was previously "syntax_and_range".)

is_integer: BOOLEAN

-- Does `Current' represent an INTEGER?

ensure

definition:

-- Result is true if and only if the following two

-- conditions are satisfied:

--

-- 1. In the following BNF grammar, the value of

-- `Current' can be produced by "Integer_literal":

--

-- Integer_literal = [Sign] Integer

-- Sign = "+" | "-"

-- Integer = Digit | Digit Integer

-- Digit = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9"

--

-- 2. The integer value represented by `Current'

-- is within the (inclusive) range

-- minimum_integer..maximum_integer

-- where `minimum_integer' and `maximum_integer'

-- are the constants defined in class PLATFORM.

(The tag was previously "syntax_and_range".)

is_real: BOOLEAN

-- Does `Current' represent a REAL?

ensure

definition:

-- Result is true if and only if the following two

-- conditions are satisfied:

--

-- 1. In the following BNF grammar, the value of

-- `Current' can be produced by "Real_literal":

--

-- Real_literal = Mantissa [Exponent_part]

-- Exponent_part = "E" Exponent

-- | "e" Exponent

-- Exponent = Integer_literal

-- Mantissa = Decimal_literal

-- Decimal_literal = Integer_literal ["." Integer]

-- Integer_literal = [Sign] Integer

-- Sign = "+" | "-"

-- Integer = Digit | Digit Integer

-- Digit = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9"

--

-- 2. The numerical value represented by `Current'

-- is within the range that can be represented

-- by an instance of type REAL.

(The tag was previously "syntax_and_range".)

to_boolean: BOOLEAN

-- Boolean value;

-- "true" yields true, "false" yields false

require

represents_a_boolean: is_boolean

ensure

definition: Result = same_string("true")

(The tag was previously "to_boolean".)

Regards,

Roger

--

Roger Browne - roger@... - Everything Eiffel

19 Eden Park Lancaster LA1 4SJ UK - Phone +44 1524 32428- There was no further discussion on the proposal to change several tag

names to 'definition', so I'm going to close this off now.

****************************************************************

* I am not aware of any objections to the following proposal. *

* I will incorporate it into the working draft without a *

* poll, unless someone requests a formal poll. *

****************************************************************

> 28 JANUARY 2002 VERSIONS (CLASS ARRAY):

Regards,

>

> count: INTEGER

> -- Number of available indices

> ensure

> definition: Result = upper - lower + 1

>

> (The tag was previously "consistent_with_bounds".)

>

> 28 JANUARY 2002 VERSIONS (CLASS STRING):

>

> is_boolean: BOOLEAN

> -- Does `Current' represent a BOOLEAN?

> ensure

> definition: Result = (same_string("true")

> or same_string("false"))

>

> (The tag was previously "is_boolean".)

>

> is_double: BOOLEAN

> -- Does `Current' represent a DOUBLE?

> ensure

> definition:

> -- Result is true if and only if the following two

> -- conditions are satisfied:

> --

> -- 1. In the following BNF grammar, the value of

> -- `Current' can be produced by "Real_literal":

> --

> -- Real_literal = Mantissa [Exponent_part]

> -- Exponent_part = "E" Exponent

> -- | "e" Exponent

> -- Exponent = Integer_literal

> -- Mantissa = Decimal_literal

> -- Decimal_literal = Integer_literal ["." Integer]

> -- Integer_literal = [Sign] Integer

> -- Sign = "+" | "-"

> -- Integer = Digit | Digit Integer

> -- Digit = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9"

> --

> -- 2. The numerical value represented by `Current'

> -- is within the range that can be represented

> -- by an instance of type DOUBLE.

>

> (The tag was previously "syntax_and_range".)

>

> is_integer: BOOLEAN

> -- Does `Current' represent an INTEGER?

> ensure

> definition:

> -- Result is true if and only if the following two

> -- conditions are satisfied:

> --

> -- 1. In the following BNF grammar, the value of

> -- `Current' can be produced by "Integer_literal":

> --

> -- Integer_literal = [Sign] Integer

> -- Sign = "+" | "-"

> -- Integer = Digit | Digit Integer

> -- Digit = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9"

> --

> -- 2. The integer value represented by `Current'

> -- is within the (inclusive) range

> -- minimum_integer..maximum_integer

> -- where `minimum_integer' and `maximum_integer'

> -- are the constants defined in class PLATFORM.

>

> (The tag was previously "syntax_and_range".)

>

> is_real: BOOLEAN

> -- Does `Current' represent a REAL?

> ensure

> definition:

> -- Result is true if and only if the following two

> -- conditions are satisfied:

> --

> -- 1. In the following BNF grammar, the value of

> -- `Current' can be produced by "Real_literal":

> --

> -- Real_literal = Mantissa [Exponent_part]

> -- Exponent_part = "E" Exponent

> -- | "e" Exponent

> -- Exponent = Integer_literal

> -- Mantissa = Decimal_literal

> -- Decimal_literal = Integer_literal ["." Integer]

> -- Integer_literal = [Sign] Integer

> -- Sign = "+" | "-"

> -- Integer = Digit | Digit Integer

> -- Digit = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9"

> --

> -- 2. The numerical value represented by `Current'

> -- is within the range that can be represented

> -- by an instance of type REAL.

>

> (The tag was previously "syntax_and_range".)

>

> to_boolean: BOOLEAN

> -- Boolean value;

> -- "true" yields true, "false" yields false

> require

> represents_a_boolean: is_boolean

> ensure

> definition: Result = same_string("true")

>

> (The tag was previously "to_boolean".)

Roger

--

Roger Browne - roger@... - Everything Eiffel

19 Eden Park Lancaster LA1 4SJ UK - Phone +44 1524 32428