note description: "Messages used in AutoProof." date: "$Date$" revision: "$Revision$" frozen class E2B_MESSAGES inherit SHARED_LOCALE feature -- Validity error messages functional_feature_not_function: STRING_32 do Result := locale.translation_in_context ("Functional feature has to be a pure function.", "autoproof") end functional_feature_not_single_assignment: STRING_32 do Result := locale.translation_in_context ("A functional feature has to consist of exactly one assignment to the Result (and optional check instructions before the assignment).", "autoproof") end functional_feature_redefined: STRING_32 do Result := locale.translation_in_context ("Functional feature cannot be redefined.", "autoproof") end pure_function_has_mods: STRING_32 do Result := locale.translation_in_context ("Function with a non-empty modify clause has to be declared impure.", "autoproof") end impure_function_in_contract (a_fname: READABLE_STRING_32): STRING_32 do Result := locale.formatted_string ("Impure function '$1' cannot be used in specifications.", a_fname) end invalid_call_in_invariant: STRING_32 do Result := locale.translation_in_context ("Class invariant must not access built-in attributes closed or owner, or functions marked inv_unfriendly.", "autoproof") end invalid_call_in_friendly_function: STRING_32 do Result := locale.translation_in_context ("A pure function must not access built-in attributes closed or owner, or functions marked inv_unfriendly, unless it is itself inv_unfriendly.", "autoproof") end creator_call_as_procedure (a_pname: READABLE_STRING_32): STRING_32 do Result := locale.formatted_string ("Feature '$1' is a creator but is called as a regular procedure.", a_pname) end nonsetter_call_from_setter (a_pname: READABLE_STRING_32): STRING_32 do Result := locale.formatted_string ("A non-setter procedure '$1' is called from a setter procedure.", a_pname) end first_argument_string: STRING_32 do Result := locale.translation_in_context ("First argument has to be a manifest string.", "autoproof") end first_argument_string_or_tuple: STRING_32 do Result := locale.translation_in_context ("First argument has to be a manifest string or a tuple of manifest strings.", "autoproof") end unknown_feature (a_fname, a_cname: READABLE_STRING_32): STRING_32 do Result := locale.formatted_string ("Feature '$1' is not found in class '$2'.", a_fname, a_cname) end unknown_attribute (a_fname, a_cname: READABLE_STRING_32): STRING_32 do Result := locale.formatted_string ("Feature '$1' is not an attribute of class '$2'.", a_fname, a_cname) end unknown_model (a_fname, a_cname: READABLE_STRING_32): STRING_32 do Result := locale.formatted_string ("Feature '$1' is not a model attribute of class '$2'.", a_fname, a_cname) end invalid_model_replacement (a_fname, a_cname: READABLE_STRING_32): STRING_32 do Result := locale.formatted_string ("Feature '$1' is a model of the parent class '$2' and thus cannot be a replacemnt model.", a_fname, a_cname) end invalid_tag (a_tag, a_class_name: READABLE_STRING_32): STRING_32 do Result := locale.formatted_string ("Filtered invariant of class '$2' lists invalid tag: $1", a_tag, a_class_name) end predicate_outside_of_precondition_and_loop_invariant (a_kind: STRING): STRING_32 do Result := locale.formatted_string ("$1 clauses are only allowed in preconditions and loop invariants (will be ignored)", a_kind) end predicate_outside_of_postcondition_and_loop_invariant (a_kind: STRING): STRING_32 do Result := locale.formatted_string ("$1 clauses are only allowed in postconditions and loop invariants (will be ignored)", a_kind) end invalid_context_for_read_predicate: STRING_32 do Result := locale.translation_in_context ("Read sets are only allowed for functions (will be ignored)", "autoproof") end variant_bad_type (a_index: INTEGER): STRING_32 do Result := locale.formatted_string ("Type of variant number $1 has no well-founded order.", a_index.out) end logical_invalid_type_properties: STRING_32 do Result := locale.translation_in_context ("The number of typed properties in the logical class does not correspond to the number of generic parameters.", "autoproof") end logical_no_across_conversion: STRING_32 do Result := locale.translation_in_context ("The logical class is used in quantification but does not map its new_cursor feature to a set.", "autoproof") end guard_feature_not_predicate: STRING_32 do Result := locale.translation_in_context ("Update guard has to be of type BOOLEAN.", "autoproof") end guard_feature_arg_count: STRING_32 do Result := locale.translation_in_context ("Update guard has to have exactly two argument.", "autoproof") end guard_feature_arg1: STRING_32 do Result := locale.translation_in_context ("The first argument of an update guard has to be of the same type as the guarded attribute.", "autoproof") end guard_feature_arg2: STRING_32 do Result := locale.translation_in_context ("The second argument of an update guard has to be of type ANY.", "autoproof") end invalid_ghost_status (a_old_fname, a_old_cname: READABLE_STRING_32): STRING_32 do Result := locale.formatted_string ("Ghost status does not match previous version '$1' from class '$2'.", a_old_fname, a_old_cname) end feature -- Verification error messages check_violated: STRING_32 do Result := locale.translation_in_context ("Check may be violated (untagged).", "autoproof") end check_with_tag_violated: STRING_32 do Result := locale.translation_in_context ("Check $tag may be violated.", "autoproof") end function_precondition_violated: STRING_32 do Result := locale.translation_in_context ("Precondition may be violated on invocation of $called_feature.", "autoproof") end invariant_violated: STRING_32 do Result := locale.translation_in_context ("Invariant might not hold on call to $called_feature.", "autoproof") end invariant_with_tag_violated: STRING_32 do Result := locale.translation_in_context ("Invariant $tag might not hold on call to $called_feature.", "autoproof") end precondition_violated: STRING_32 do Result := locale.translation_in_context ("Precondition may be violated on call to $called_feature (untagged).", "autoproof") end precondition_with_tag_violated: STRING_32 do Result := locale.translation_in_context ("Precondition $tag may be violated on call to $called_feature.", "autoproof") end postcondition_violated: STRING_32 do Result := locale.translation_in_context ("Postcondition may be violated (untagged).", "autoproof") end postcondition_with_tag_violated: STRING_32 do Result := locale.translation_in_context ("Postcondition $tag may be violated.", "autoproof") end loop_inv_violated_on_entry: STRING_32 do Result := locale.translation_in_context ("Loop invariant may be violated on entry (untagged).", "autoproof") end loop_inv_with_tag_violated_on_entry: STRING_32 do Result := locale.translation_in_context ("Loop invariant $tag may be violated on entry.", "autoproof") end loop_inv_not_maintained: STRING_32 do Result := locale.translation_in_context ("Loop invariant may not be maintained (untagged).", "autoproof") end loop_inv_with_tag_not_maintained: STRING_32 do Result := locale.translation_in_context ("Loop invariant $tag may not be maintained.", "autoproof") end void_call: STRING_32 do Result := locale.translation_in_context ("Possible Void call.", "autoproof") end void_call_in_precondition: STRING_32 do Result := locale.translation_in_context ("Possible Void call in precondition on call to $called_feature (untagged).", "autoproof") end void_call_in_precondition_with_tag: STRING_32 do Result := locale.translation_in_context ("Possible Void call in precondition $tag on call to $called_feature.", "autoproof") end void_call_in_postcondition: STRING_32 do Result := locale.translation_in_context ("Possible Void call in postcondition (untagged).", "autoproof") end void_call_in_postcondition_with_tag: STRING_32 do Result := locale.translation_in_context ("Possible Void call in postcondition $tag.", "autoproof") end decreases_not_decreasing: STRING_32 do Result := locale.translation_in_context ("Variant may not decrease at this recursive call / the end of this loop body.", "autoproof") end decreases_bounded: STRING_32 do Result := locale.translation_in_context ("Integer variant component at position $variant may be negative.", "autoproof") end overflow: STRING_32 do Result := locale.translation_in_context ("Possible arithmetic overflow.", "autoproof") end overflow_in_precondition: STRING_32 do Result := locale.translation_in_context ("Possible arithmetic overflow in precondition on call to $called_feature (untagged).", "autoproof") end overflow_in_precondition_with_tag: STRING_32 do Result := locale.translation_in_context ("Possible arithmetic overflow in precondition $tag on call to $called_feature.", "autoproof") end overflow_in_postcondition: STRING_32 do Result := locale.translation_in_context ("Possible arithmetic overflow in postcondition (untagged).", "autoproof") end overflow_in_postcondition_with_tag: STRING_32 do Result := locale.translation_in_context ("Possible arithmetic overflow in postcondition $tag.", "autoproof") end assignment_attached_and_allocated: STRING_32 do Result := locale.translation_in_context ("Target of assignment may not be attached or allocated", "autoproof") end assignment_closed_or_owner_not_allowed: STRING_32 do Result := locale.translation_in_context ("The fields `closed' and `owner' cannot be directly assigned.", "autoproof") end assignment_target_open: STRING_32 do Result := locale.translation_in_context ("Target of assignment may not be open.", "autoproof") end assignment_observers_open_or_guard_holds: STRING_32 do Result := locale.translation_in_context ("Observers of the assignment target may be invalidated.", "autoproof") end assignment_attribute_writable: STRING_32 do Result := locale.translation_in_context ("Target attribute may not be writable.", "autoproof") end access_attribute_readable: STRING_32 do Result := locale.translation_in_context ("Attribute $called_feature might not be readable.", "autoproof") end access_frame_readable: STRING_32 do Result := locale.translation_in_context ("Some members of the read frame of $called_feature might not be readable.", "autoproof") end ownership_explicit_note: STRING_32 do Result := locale.translation_in_context ("Disable this default by making $explicit_value explicit.", "autoproof") end feature -- Other boogie_launch_failed (a_executable: READABLE_STRING_32): STRING_32 do Result := locale.formatted_string ("Launching Boogie failed (command was '$1').", a_executable) end internal_translation_error (a_unit_id: READABLE_STRING_32): STRING_32 do Result := locale.formatted_string ("Translation of '$1' failed due to an internal error.", a_unit_id) end feature -- GUI tool_header_class: STRING_32 do Result := locale.translation_in_context ("Class", "autoproof") end tool_header_feature: STRING_32 do Result := locale.translation_in_context ("Feature", "autoproof") end tool_header_information: STRING_32 do Result := locale.translation_in_context ("Information", "autoproof") end tool_header_position: STRING_32 do Result := locale.translation_in_context ("Position", "autoproof") end tool_header_time: STRING_32 do Result := locale.translation_in_context ("Time [s]", "autoproof") end tool_successful_button (a_value: INTEGER): STRING_32 do Result := locale.formatted_string ("$1 Successful", a_value) end tool_failed_button (a_value: INTEGER): STRING_32 do Result := locale.formatted_string ("$1 Failed", a_value) end tool_error_button (a_value: INTEGER): STRING_32 do Result := locale.formatted_string (locale.plural_translation ("$1 Error", "$1 Errors", a_value), a_value) end tool_text_filter: STRING_32 do Result := locale.translation_in_context ("Filter", "autoproof") end status_translating (a_current, a_total: INTEGER): STRING_32 do Result := locale.formatted_string ("Translating Eiffel to Boogie ($1/$2 elements remaining)", a_current, a_total) end status_boogie_running (a_milliseconds: INTEGER): STRING_32 do Result := locale.formatted_string ("Boogie running: $1 s", a_milliseconds // 1000) end status_boogie_finished (a_milliseconds: INTEGER): STRING_32 do Result := locale.formatted_string ("Boogie finished: $1 s", a_milliseconds // 1000) end end