Loading ...
Sorry, an error occurred while loading the content.

Postcondition tag name for queries: "definition"

Expand Messages
  • Roger Browne
    ... OK, there seems to be general agreement on this style guideline. At the end of this message I have shown how existing features of STRING and ARRAY would
    Message 1 of 2 , Jan 28, 2002
    • 0 Attachment
      > Peter Horan 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?

      James McKim wrote:
      > I agree, I prefer the word "definition" when we have one line that is
      > defining a query.

      OK, there seems to be general agreement on this style guideline. At the
      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
      > 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.

      Although the group decided not to include this directed graph within the
      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
    • Roger Browne
      There was no further discussion on the proposal to change several tag names to definition , so I m going to close this off now.
      Message 2 of 2 , Feb 5 9:13 AM
      • 0 Attachment
        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):
        >
        > 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
      Your message has been successfully submitted and would be delivered to recipients shortly.