note description: "Result of verifying an individual procedure in a Boogie program." date: "$Date$" revision: "$Revision$" class E2B_BOOGIE_PROCEDURE_RESULT create make feature {NONE} -- Initialization make (a_name: STRING; a_context: E2B_BOOGIE_RESULT) -- Initialize procedure result do name := a_name.twin context := a_context create errors.make end feature -- Access name: STRING -- Name of verified procedure. time: REAL -- Time of verification in seconds. errors: LINKED_LIST [E2B_BOOGIE_PROCEDURE_ERROR] -- List of verification errors. context: E2B_BOOGIE_RESULT -- Context of this result. feature -- Status report is_successful: BOOLEAN -- Is this procedure verified successfuly? is_error: BOOLEAN -- Is verification of this procedure failed? is_inconclusive: BOOLEAN -- Is verification of this procedure inconclusive? feature -- Status setting set_successful -- Set `is_successful' to true. do is_successful := True end set_error -- Set `is_error' to true. do is_error := True end set_inconclusive -- Set `is_inconclusive' to true. do is_inconclusive := True end feature -- Element change set_time (a_value: REAL) -- Set `time' to `a_value'. do time := a_value end invariant no_errors_when_successful: is_successful implies errors.is_empty no_errors_when_inconclusive: is_inconclusive implies errors.is_empty end