Pylon: a foundation library ~ User's guide (Chapter 3) -- contents | previous | next
deferred class interface P_TEXT_OBJECT
indexing
cluster: pylon, misc;
description: "Text (ASCII) representation of an object (in/out)";
interface: inheritance;
feature specification
-- Public interface
to_string : STRING
ensure
is_copy : Result /= void;
from_string (str : STRING)
-- Init object from string.
require
valid : str /= void;
ensure
done : -- success implies to_string.is_equal(str)
feature specification {PUBLIC_NONE}
-- Methods to effect
object_to_string (tm : P_TEXT_OBJECT_MANAGER)
-- Convert object to string format thanks to
-- the 'tm' facility.
require
valid_manager : tm /= void;
deferred
string_to_object (tm : P_TEXT_OBJECT_MANAGER)
-- Convert string to object thanks to the 'tm'
-- facility. The heir shall check if 'tm' can parse
-- succesfully the input string and maintain the
-- invariant otherwise.
require
valid_manager : tm /= void;
deferred
end interface -- class P_TEXT_OBJECT
class interface P_TEXT_OBJECT_MANAGER
indexing
cluster: pylon, misc;
description: "Text object support";
interface: client;
feature specification
-- Input
is_output : BOOLEAN
-- Is the manager in output mode?
put_boolean (bool : BOOLEAN)
-- Put a boolean value in the output string.
require
out : is_output;
put_character (char : CHARACTER)
-- Put a character in the output string.
require
out : is_output;
put_integer (int : INTEGER)
-- Put an integer in the output string.
put_string (outs : STRING)
-- Put a data string in the output string.
require
out : is_output;
valid_out : outs /= void;
put_object (obj : P_TEXT_OBJECT)
-- Put an encoded object in the output string.
require
out : is_output;
valid_obj : obj /= void;
put_real (number : REAL)
-- Put a real in the output string.
require
out : is_output;
put_double (number : DOUBLE)
-- Put a double in the output string.
require
out : is_output;
feature specification
-- Input
in_success : BOOLEAN
is_input : BOOLEAN
-- Is the manager in input mode?
get_boolean
-- Retrieve boolean value from stream.
require
in : is_input;
ensure
has_result : -- last_boolean set
last_boolean : BOOLEAN
get_character
-- Retrieve character from stream.
require
in : is_input;
ensure
has_result : -- last_character set.
last_character : CHARACTER
get_integer
-- Retrieve integer from stream.
require
in : is_input;
ensure
has_result : -- last_integer set.
last_integer : INTEGER
get_string
-- Retrieve string from stream.
require
in : is_input;
ensure
has_result : -- last_string set.
last_string : STRING
get_object (obj_to_change : P_TEXT_OBJECT)
-- Retrieve encoded object string, and adapt consequently
-- object given as parameter.
require
in : is_input;
get_real
-- Retrieve real number from string.
require
in : is_input;
ensure
has_result : -- last_real set.
last_real : REAL
get_double
-- Retrieve double precision real number from stream.
require
in : is_input;
ensure
has_result : -- last_double set.
last_double : DOUBLE
end interface -- class P_TEXT_OBJECT_MANAGER
class interface P_DATE
indexing
cluster: pylon, time;
description: "Gregorian date";
interface: client;
feature specification
-- Comparison
infix "<" (other : like Current) : BOOLEAN
-- Is `Current' strictly less than `other'?
-- This features determines the total ordering.
--
-- Redefined from PART_COMPARABLE to strengthen the
-- postcondition.
require
other_not_void : other /= void;
ensure
other_not_less_or_equal : Result = (not (other <= Current));
consistent : Result implies (not (other <= Current));
not_reflexive : (Current = other) implies (not Result);
is_equal (other : like Current) : BOOLEAN
-- Is `other' attached to an object considered equal to `Current'?
require
other_not_void : other /= void;
ensure
consistent : standard_is_equal (other) implies Result;
same_type : Result implies same_type (other);
symmetric : Result implies other.is_equal (Current);
feature specification
-- Hashable
hash_code : INTEGER
-- Hash_code value
ensure
non_negative : Result >= 0;
feature specification {PUBLIC_NONE}
-- Text object
object_to_string (tm : P_TEXT_OBJECT_MANAGER)
-- Convert object to string format thanks to
-- the 'tm' facility.
require
valid_manager : tm /= void;
string_to_object (tm : P_TEXT_OBJECT_MANAGER)
-- Convert string to object thanks to the 'tm'
-- facility. The heir shall check if 'tm' can parse
-- succesfully the input string and maintain the
-- invariant otherwise.
require
valid_manager : tm /= void;
feature specification
year : INTEGER
month : INTEGER
day : INTEGER
day_of_year : INTEGER
-- Day of year.
require
valid : is_valid;
ensure
valid : (Result > 0) and (Result <= 366);
day_of_week : INTEGER
-- Day of week (0 = Sunday).
require
valid : is_valid;
modern : year > 1752;
-- and not russia < 19xx ...
ensure
valid : (Result >= 0) and (Result < 7);
feature specification
set_year (yyyy : INTEGER)
-- Set year.
require
positive : yyyy > 0;
ensure
done : yyyy = year;
set_month (mm : INTEGER)
-- Set month.
require
valid : (mm >= 1) and (mm <= 12);
ensure
done : mm = month;
set_day (dd : INTEGER)
-- Set day.
require
valid : (dd >= 1) and (dd <= 31);
ensure
done : dd = day;
set (yyyy, mm, dd : INTEGER)
-- Set date.
require
valid_date : is_valid_date (yyyy, mm, dd);
ensure
done : ((dd = day) and (mm = month)) and (yyyy = year);
valid : is_valid;
feature specification
-- Status
is_valid_date (yyyy, mm, dd : INTEGER) : BOOLEAN
-- Is the given date valid.
is_valid : BOOLEAN
-- Is the current date valid?
is_leap_year : BOOLEAN
-- Is the current year a leap year?
feature specification
-- Output
out : STRING
-- New string containing a terse printable representation of
-- `Current', field by field.
--
-- `standard_out' not in ELKS_95; `out' is.
ensure
not_void : Result /= void;
to_iso_long : STRING
-- Output date in verbose ISO format.
-- eg: "1887-07-26"
require
ok : is_valid;
ensure
is_copy : Result /= void;
to_iso : STRING
-- Output date in compact ISO format.
-- eg: "18870726"
require
ok : is_valid;
ensure
is_copy : Result /= void;
to_rfc : STRING
-- Output date in canonical RFC 822 format.
-- eg: "26 Jul 1887", in English.
require
ok : is_valid;
ensure
is_copy : Result /= void;
to_european : STRING
-- Output date using usual numeric european format.
-- eg: "26/07/1887"
require
ok : is_valid;
ensure
is_copy : Result /= void;
to_american : STRING
-- Output date using usual numeric american format.
-- eg: "07/26/1887"
require
ok : is_valid;
ensure
is_copy : Result /= void;
feature specification
-- Public interface
to_string : STRING
ensure
is_copy : Result /= void;
from_string (str : STRING)
-- Init object from string.
require
valid : str /= void;
ensure
done : -- success implies to_string.is_equal(str)
feature specification
-- Features from PART_COMPARABLE
infix "<=" (other : like Current) : BOOLEAN
-- Is `Current' less than or equal to `other'?
--
-- Effects the deferred feature from PART_COMPARABLE.
require
other_not_void : other /= void;
ensure
other_not_less : Result = (not (other < Current));
consistent : Result implies (not (other < Current));
reflexive : (Current = other) implies Result;
feature specification
-- Other useful features for comparable objects.
three_way_compare (other : like Current) : INTEGER
-- Compare `Current' with `other':
-- `-1' if `Current < other';
-- `0' if `Current = other';
-- `1' if `Current > other'.
require
other_not_void : other /= void;
ensure
negative_condition : (Result = (- 1)) = (Current < other);
equal_zero : (Result = 0) = (not ((Current < other) or (Current > other)));
positive_condition : (Result = 1) = (Current > other);
min (other : like Current) : like Current
-- The smaller of `Current' and `other'.
require
other_not_void : other /= void;
ensure
less_or_equal_both : (Result <= Current) and then (Result <= other);
one_or_the_other : (three_way_compare (Result) = 0) or else (other.three_way_compare (Result) = 0);
max (other : like Current) : like Current
-- The larger of `Current' and `other'.
require
other_not_void : other /= void;
ensure
greater_or_equal_both : (Result >= Current) and then (Result >= other);
one_or_the_other : (three_way_compare (Result) = 0) or else (other.three_way_compare (Result) = 0);
feature specification
-- Effective routines whose behavior are implied by the behavior of
-- `infix "<"' and `infix "<="'.
infix ">" (other : like Current) : BOOLEAN
-- Is `Current' strictly greater than `other'?
require
other_not_void : other /= void;
ensure
other_is_less : Result = (other < Current);
infix ">=" (other : like Current) : BOOLEAN
-- Is `Current' greater than or equal to `other'?
require
other_not_void : other /= void;
ensure
other_less_or_equal : Result = (other <= Current);
end interface -- class P_DATE
class interface P_TIME
indexing
cluster: pylon, time;
description: "24 hours time";
interface: client;
feature specification
-- Comparison
infix "<" (other : like Current) : BOOLEAN
-- Is `Current' strictly less than `other'?
-- This features determines the total ordering.
--
-- Redefined from PART_COMPARABLE to strengthen the
-- postcondition.
require
other_not_void : other /= void;
ensure
other_not_less_or_equal : Result = (not (other <= Current));
consistent : Result implies (not (other <= Current));
not_reflexive : (Current = other) implies (not Result);
is_equal (other : like Current) : BOOLEAN
-- Is `other' attached to an object considered equal to `Current'?
require
other_not_void : other /= void;
ensure
consistent : standard_is_equal (other) implies Result;
same_type : Result implies same_type (other);
symmetric : Result implies other.is_equal (Current);
feature specification
-- Hashable
hash_code : INTEGER
-- Hash_code value
ensure
non_negative : Result >= 0;
feature specification {PUBLIC_NONE}
-- Text object
object_to_string (tm : P_TEXT_OBJECT_MANAGER)
-- Convert object to string format thanks to
-- the 'tm' facility.
require
valid_manager : tm /= void;
string_to_object (tm : P_TEXT_OBJECT_MANAGER)
-- Convert string to object thanks to the 'tm'
-- facility. The heir shall check if 'tm' can parse
-- succesfully the input string and maintain the
-- invariant otherwise.
require
valid_manager : tm /= void;
feature specification
-- Status
hour : INTEGER
minute : INTEGER
second : INTEGER
set_hour (hh : INTEGER)
-- Set hour.
require
valid : (hh >= 0) and (hh < 24);
ensure
done : hh = hour;
set_minute (mm : INTEGER)
-- Set minute.
require
valid : (mm >= 0) and (mm < 60);
ensure
done : mm = minute;
set_second (ss : INTEGER)
-- Set second.
require
valid : (ss >= 0) and (ss < 60);
ensure
done : ss = second;
set (hh, mm, ss : INTEGER)
-- Set time.
require
valid_hour : (hh >= 0) and (hh < 24);
valid_minute : (mm >= 0) and (mm < 60);
valid_second : (ss >= 0) and (ss < 60);
ensure
done : ((hour = hh) and (minute = mm)) and (second = ss);
feature specification
-- Status
hour_12 : INTEGER
-- Hour in am/pm format.
ensure
done : (Result >= 1) and (Result <= 12);
is_am : BOOLEAN
-- Is morning?
is_pm : BOOLEAN
-- Is evening?
feature specification
-- Output
out : STRING
-- Default string representation: ISO format.
ensure
not_void : Result /= void;
to_iso : STRING
-- Output time in ISO format.
-- eg: "233000"
ensure
is_copy : Result /= void;
to_rfc : STRING
-- Output time in RFC format.
-- eg: "23:30:00"
ensure
is_copy : Result /= void;
feature specification
-- Features from PART_COMPARABLE
infix "<=" (other : like Current) : BOOLEAN
-- Is `Current' less than or equal to `other'?
--
-- Effects the deferred feature from PART_COMPARABLE.
require
other_not_void : other /= void;
ensure
other_not_less : Result = (not (other < Current));
consistent : Result implies (not (other < Current));
reflexive : (Current = other) implies Result;
feature specification
-- Other useful features for comparable objects.
three_way_compare (other : like Current) : INTEGER
-- Compare `Current' with `other':
-- `-1' if `Current < other';
-- `0' if `Current = other';
-- `1' if `Current > other'.
require
other_not_void : other /= void;
ensure
negative_condition : (Result = (- 1)) = (Current < other);
equal_zero : (Result = 0) = (not ((Current < other) or (Current > other)));
positive_condition : (Result = 1) = (Current > other);
min (other : like Current) : like Current
-- The smaller of `Current' and `other'.
require
other_not_void : other /= void;
ensure
less_or_equal_both : (Result <= Current) and then (Result <= other);
one_or_the_other : (three_way_compare (Result) = 0) or else (other.three_way_compare (Result) = 0);
max (other : like Current) : like Current
-- The larger of `Current' and `other'.
require
other_not_void : other /= void;
ensure
greater_or_equal_both : (Result >= Current) and then (Result >= other);
one_or_the_other : (three_way_compare (Result) = 0) or else (other.three_way_compare (Result) = 0);
feature specification
-- Effective routines whose behavior are implied by the behavior of
-- `infix "<"' and `infix "<="'.
infix ">" (other : like Current) : BOOLEAN
-- Is `Current' strictly greater than `other'?
require
other_not_void : other /= void;
ensure
other_is_less : Result = (other < Current);
infix ">=" (other : like Current) : BOOLEAN
-- Is `Current' greater than or equal to `other'?
require
other_not_void : other /= void;
ensure
other_less_or_equal : Result = (other <= Current);
feature specification
-- Public interface
to_string : STRING
ensure
is_copy : Result /= void;
from_string (str : STRING)
-- Init object from string.
require
valid : str /= void;
ensure
done : -- success implies to_string.is_equal(str)
invariant
hour : (hour >= 0) and (hour < 24);
minute : (minute >= 0) and (minute < 60);
second : (second >= 0) and (second < 60);
ampm : is_am xor is_pm;
end interface -- class P_TIME
class interface P_DATE_TIME
indexing
cluster: pylon, time;
description: "Date and time";
interface: client;
creation
make
feature specification
-- Creation
make
feature specification
-- Comparison
is_equal (other : like Current) : BOOLEAN
-- Is `other' attached to an object considered equal to `Current'?
require
other_not_void : other /= void;
ensure
consistent : standard_is_equal (other) implies Result;
same_type : Result implies same_type (other);
symmetric : Result implies other.is_equal (Current);
feature specification
-- Hashable
hash_code : INTEGER
-- Hash_code value
ensure
non_negative : Result >= 0;
feature specification {PUBLIC_NONE}
-- Text object
object_to_string (tm : P_TEXT_OBJECT_MANAGER)
-- Convert object to string format thanks to
-- the 'tm' facility.
require
valid_manager : tm /= void;
string_to_object (tm : P_TEXT_OBJECT_MANAGER)
-- Convert string to object thanks to the 'tm'
-- facility. The heir shall check if 'tm' can parse
-- succesfully the input string and maintain the
-- invariant otherwise.
require
valid_manager : tm /= void;
feature specification
date : P_DATE
time : P_TIME
set_date (yyyy, mm, dd : INTEGER)
-- Set date.
require
valid : -- see DATE.set
ensure
done : date.is_valid;
set_time (hh, mm, ss : INTEGER)
require
valid : -- see TIME.set
set (yyyy, mo, dd : INTEGER; hh, mi, ss : INTEGER)
require
valid : -- see DATE.set and TIME.set
ensure
done : date.is_valid;
feature specification
-- Status
is_valid : BOOLEAN
-- Is the current object holding valid date & time?
is_local : BOOLEAN
-- Do this date and time have NO timezone information attached?
feature specification
-- Timezone
is_utc : BOOLEAN
-- Is the current time zone UTC (GMT)?
require
has_tz : not is_local;
ensure
done : (Result = true) = (timezone_bias = 0);
timezone_bias : INTEGER
require
has_tz : not is_local;
set_timezone_bias (bias : INTEGER)
-- Timezone bias used to convert from the current time to GMT in
-- minutes.
require
bounds : (bias < 1440) and (bias > (- 1440));
ensure
not_local : not is_local;
feature specification
-- Output
to_iso : STRING
-- Output date and time in ISO 8601 format.
out : STRING
-- Output date and time in ISO 8601 format.
ensure
not_void : Result /= void;
to_iso_long : STRING
-- Output date in ISO verbose format.
to_rfc : STRING
-- Output date & time in RFC format.
feature specification
-- Public interface
to_string : STRING
ensure
is_copy : Result /= void;
from_string (str : STRING)
-- Init object from string.
require
valid : str /= void;
ensure
done : -- success implies to_string.is_equal(str)
invariant
valid_date : date /= void;
valid_time : time /= void;
end interface -- class P_DATE_TIME
class interface P_PAIR [I, J]
indexing
cluster: pylon;
description: "Generic pair";
interface: client;
feature specification
-- Elements
one : I
two : J
feature specification
-- Change
set_one (o : I)
ensure
keep_reference : one = o;
set_two (t : J)
ensure
keep_reference : two = t;
end interface -- class P_PAIR
class interface P_INTEGER_DECODER
indexing
cluster: pylon, format;
description: "Decode string to integers in base 2-36";
interface: client;
creation
make
feature specification
-- Creation
make (new_base : INTEGER)
require
ok : new_base > 2;
feature specification
-- Base
base : INTEGER
feature specification
-- Integer
extend (digit : CHARACTER)
-- Add right digit.
require
base : is_digit (digit);
ensure
done_integer : -- value = ((old value) * base + char_to_int(digit))
done_digits : -- digits = old digits + 1
reset
ensure
ok : (value = 0) and (digits = 0);
value : INTEGER
digits : INTEGER
feature specification
-- String to integer
from_string (str : STRING)
require
ok : str /= void;
feature specification
-- Digit level
int_to_char (digit : INTEGER) : CHARACTER
-- Integer to character digit.
require
ok : (digit >= 0) and (digit < base);
ensure
good_base : is_digit (Result);
done : char_to_int (Result) = digit;
char_to_int (c : CHARACTER) : INTEGER
-- Character to integer.
require
is_intchar : is_digit (c);
ensure
good_base : (Result >= 0) and (Result < base);
done : int_to_char (Result) = c;
is_digit (c : CHARACTER) : BOOLEAN
-- Is this character a valid digit?
feature specification
-- Encode
value_to_string (int : INTEGER) : STRING
-- Encode character.
ensure
is_copy : Result /= void;
done : Result.count > 0;
invariant
base_ok : (base >= 2) and (base <= digit_table.count);
end interface -- class P_INTEGER_DECODER