class interface
HTML_TABLE
create
make (nb_row, nb_col: INTEGER)
feature
initialize (v: STRING)
v
ARRAY2
array2_make (nb_rows, nb_columns: INTEGER)
nb_rows
nb_columns
ARRAY2
require ARRAY2
not_flat: nb_rows > 0
not_thin: nb_columns > 0
ensure ARRAY2
new_count: count = height * width
make_from_array (a: ARRAY [STRING])
a
ARRAY
ARRAY
require ARRAY
array_exists: a /= void
feature
entry (i: INTEGER): STRING
i
ARRAY
require ARRAY
valid_key: valid_index (i)
has (v: STRING): BOOLEAN
v
object_comparison
ARRAY
ensure CONTAINER
not_found_in_empty: Result implies not is_empty
item (row, column: INTEGER): STRING
rowcolumn
ARRAY2
require ARRAY2
valid_row: (1 <= row) and (row <= height)
valid_column: (1 <= column) and (column <= width)
infix "@" (i: INTEGER): STRING
i
ARRAYitem
ARRAY
require TABLE
valid_key: valid_index (k)
feature
area: SPECIAL [STRING]
TO_SPECIAL
feature
additional_space: INTEGER
RESIZABLE
ensure RESIZABLE
at_least_one: Result >= 1
capacity: INTEGER
ARRAYcount
ARRAY
ensure then ARRAY
consistent_with_bounds: Result = upper - lower + 1
count: INTEGER
ARRAYcapacity
ARRAY
ensure then ARRAY
consistent_with_bounds: Result = upper - lower + 1
Growth_percentage: INTEGER is 50
RESIZABLE
height: INTEGER
ARRAY2
index_set: INTEGER_INTERVAL
ARRAY
ensure INDEXABLE
not_void: Result /= void
ensure then ARRAY
same_count: Result.count = count
same_bounds: ((Result.lower = lower) and (Result.upper = upper))
lower: INTEGER
ARRAY
Minimal_increase: INTEGER is 5
RESIZABLE
occurrences (v: STRING): INTEGER
v
ARRAY
ensure BAG
non_negative_occurrences: Result >= 0
upper: INTEGER
ARRAY
width: INTEGER
ARRAY2
feature
is_equal (other: like Current): BOOLEAN
other
ARRAY
require ANY
other_not_void: other /= void
ensure ANY
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result
feature
all_default: BOOLEAN
ARRAY
ensure ARRAY
definition: Result = (count = 0 or else ((array_item (upper) = void or else array_item (upper) = array_item (upper).default) and subarray (lower, upper - 1).all_default))
changeable_comparison_criterion: BOOLEAN
object_comparison
CONTAINER
extendible: BOOLEAN
ARRAY
full: BOOLEAN
ARRAY
is_empty: BOOLEAN
FINITE
is_inserted (v: STRING): BOOLEAN
v
COLLECTION
object_comparison: BOOLEAN
equal=
=
CONTAINER
prunable: BOOLEAN
ARRAY
resizable: BOOLEAN
capacity
RESIZABLE
same_items (other: like Current): BOOLEAN
other
ARRAY
require ARRAY
other_not_void: other /= void
ensure ARRAY
definition: Result = ((count = other.count) and then (count = 0 or else (array_item (upper) = other.array_item (other.upper) and subarray (lower, upper - 1).same_items (other.subarray (other.lower, other.upper - 1)))))
valid_index (i: INTEGER): BOOLEAN
i
ARRAY
ensure then INDEXABLE
only_if_in_index_set: Result implies ((i >= index_set.lower) and (i <= index_set.upper))
valid_index_set: BOOLEAN
ARRAY
feature
compare_objects
equal
=
CONTAINER
require CONTAINER
changeable_comparison_criterion
ensure CONTAINER
object_comparison
compare_references
=
equal
CONTAINER
require CONTAINER
changeable_comparison_criterion
ensure CONTAINER
reference_comparison: not object_comparison
feature
enter (v: like array_item; i: INTEGER)
iv
ARRAY
require ARRAY
valid_key: valid_index (i)
fill (other: CONTAINER [STRING])
other
other
COLLECTION
require COLLECTION
other_not_void: other /= void
extendible
force (v: like item; row, column: INTEGER)
vrowcolumn
ARRAY2
require ARRAY2
row_large_enough: 1 <= row
column_large_enough: 1 <= column
put (v: like item; row, column: INTEGER)
vrowcolumn
ARRAY2
require ARRAY2
valid_row: 1 <= row and row <= height
valid_column: 1 <= column and column <= width
subcopy (other: like Current; start_pos, end_pos, index_pos: INTEGER)
otherstart_posend_pos
index_pos
ARRAY
require ARRAY
other_not_void: other /= void
valid_start_pos: other.valid_index (start_pos)
valid_end_pos: other.valid_index (end_pos)
valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1)
valid_index_pos: valid_index (index_pos)
enough_space: (upper - index_pos) >= (end_pos - start_pos)
feature
clear_all
ARRAY
ensure ARRAY
stable_lower: lower = old lower
stable_upper: upper = old upper
default_items: all_default
discard_items
ARRAY
ensure ARRAY
default_items: all_default
prune_all (v: STRING)
v
object_comparison
COLLECTION
require COLLECTION
prunable
ensure COLLECTION
no_more_occurrences: not has (v)
wipe_out
ARRAY2
feature
automatic_grow
Growth_percentage
RESIZABLE
ensure RESIZABLE
increased_capacity: capacity >= old capacity + old capacity * growth_percentage // 100
grow (i: INTEGER)
i
ARRAY
ensure RESIZABLE
new_capacity: capacity >= i
resize (nb_rows, nb_columns: INTEGER)
nb_rowsnb_columns
ARRAY2
require ARRAY2
valid_row: nb_rows >= 1
valid_column: nb_columns >= 1
feature
to_c: ANY
ARRAY
feature
linear_representation: LINEAR [STRING]
ARRAY
feature
copy (other: like Current)
other
clone
ARRAY
require ANY
other_not_void: other /= void
type_identity: same_type (other)
ensure ANY
is_equal: is_equal (other)
ensure then ARRAY
equal_areas: area.is_equal (other.area)
subarray (start_pos, end_pos: INTEGER): like Current
start_posend_pos
ARRAY
require ARRAY
valid_start_pos: valid_index (start_pos)
valid_end_pos: valid_index (end_pos)
valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1)
ensure ARRAY
lower: Result.lower = start_pos
upper: Result.upper = end_pos
feature
Align: STRING is " ALIGN="
HTML_TABLE_CONSTANTS
Background: STRING is " BACKGROUND="
HTML_TABLE_CONSTANTS
Bgcolor: STRING is " BGCOLOR="
HTML_TABLE_CONSTANTS
Border: STRING is " BORDER="
HTML_TABLE_CONSTANTS
Bordercolor: STRING is " BORDERCOLOR="
HTML_TABLE_CONSTANTS
Bordercolordark: STRING is " BORDERCOLORDARK="
HTML_TABLE_CONSTANTS
Bordercolorlight: STRING is " BORDERCOLORLIGHT="
HTML_TABLE_CONSTANTS
Bottom: STRING is "BOTTOM"
HTML_TABLE_CONSTANTS
Caption_end: STRING is "</CAPTION>"
HTML_TABLE_CONSTANTS
Caption_start: STRING is "<CAPTION"
HTML_TABLE_CONSTANTS
Center: STRING is "CENTER"
HTML_TABLE_CONSTANTS
Col_end: STRING is "</TD>"
HTML_TABLE_CONSTANTS
Col_start: STRING is "<TD"
HTML_TABLE_CONSTANTS
Colspan: STRING is " COLSPAN="
HTML_TABLE_CONSTANTS
Left: STRING is "LEFT"
HTML_TABLE_CONSTANTS
make (nb_row, nb_col: INTEGER)
Newline: STRING is ""
HTML_TABLE_CONSTANTS
Nowrap: STRING is " NOWRAP"
HTML_TABLE_CONSTANTS
Right: STRING is "RIGHT"
HTML_TABLE_CONSTANTS
Row_end: STRING is "</TR>"
HTML_TABLE_CONSTANTS
Row_start: STRING is "<TR"
HTML_TABLE_CONSTANTS
Rowspan: STRING is " ROWSPAN="
HTML_TABLE_CONSTANTS
Table_end: STRING is "</TABLE>"
HTML_TABLE_CONSTANTS
Table_start: STRING is "<TABLE"
HTML_TABLE_CONSTANTS
Tag_end: STRING is ">"
HTML_TABLE_CONSTANTS
Tag_start: STRING is "<"
HTML_TABLE_CONSTANTS
Top: STRING is "TOP"
HTML_TABLE_CONSTANTS
Valign: STRING is " VALIGN="
HTML_TABLE_CONSTANTS
Table_width: STRING is " WIDTH="
HTML_TABLE_CONSTANTS
feature
border_value: INTEGER
caption: STRING
col_value: INTEGER
row_value: INTEGER
feature
add_col (a_row: ARRAY [STRING])
require
a_row /= void
col_value <= width
add_row (a_row: ARRAY [STRING])
require
a_row /= void
row_value <= height
put_col (a_row: ARRAY [STRING])
STRING
require
a_row /= void
col_value <= width
put_row (a_row: ARRAY [STRING])
STRING
require
a_row /= void
row_value <= height
feature STRING
attribute_out (an_attribute, its_value: STRING): STRING
attributes_out: STRING
body_out: STRING
caption_attributes_out: STRING
caption_out: STRING
col_attributes_out (row, col: INTEGER): STRING
require
row <= height
col <= width
out: STRING
STRING
row_attributes_out (row, col: INTEGER): STRING
require
row <= height
feature
set_border (n: INTEGER)
set_caption (s: STRING)
set_caption_to_bottom
set_caption_to_top
set_col (n: INTEGER)
set_row (n: INTEGER)
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
ARRAY2
items_number: count = width * height
ARRAY
area_exists: area /= void
consistent_size: capacity = upper - lower + 1
non_negative_count: count >= 0
index_set_has_same_count: valid_index_set
RESIZABLE
increase_by_at_least_one: minimal_increase >= 1
BOUNDED
valid_count: count <= capacity
full_definition: full = (count = capacity)
FINITE
empty_definition: is_empty = (count = 0)
non_negative_count: count >= 0
INDEXABLE
index_set_not_void: index_set /= void
end -- HTML_TABLE