note AutoProof: ownership, ownership_defaults, overflow class B_MESSAGES feature -- Successful verification verification_successful (a, b, c: INTEGER) require tag1: a > 0 b > 0 tag2: c > 0 do end feature -- Check violation check_fails (a: INTEGER) do check a > 0 end end tagged_check_fails (a: INTEGER) do check tag1: a > 0 end end multi_check_fails (a, b, c: INTEGER) do check tag1: a > 0 b > 0 tag2: c > 0 end end feature -- Postcondition violation postcondition_fails: INTEGER do ensure Result > 0 end tagged_postcondition_fails: INTEGER do ensure tag1: Result > 0 end multi_postcondition_fails (a: INTEGER): INTEGER do Result := a ensure tag1: Result > 0 Result < 0 end feature -- Precondition violation precondition_fails: INTEGER do verification_successful (1, 0, 1) end tagged_precondition_fails: INTEGER do verification_successful (0, 1, 1) end multi_precondition_fails (a: INTEGER): INTEGER do -- ONLY ONE ERROR REPORTED verification_successful (0, 0, 0) end feature -- Loop invariant violation loop_invariant_fails_on_entry local a: INTEGER do from invariant a < 0 until a > 10 loop a := a + 1 end end tagged_loop_invariant_fails_on_entry local a: INTEGER do from invariant tag1: a < 0 until a > 10 loop a := a + 1 end end multi_loop_invariant_fails_on_entry local a, b, c: INTEGER do from invariant -- ONLY ONE ERROR REPORTED tag1: a < 0 b < 0 tag2: c < 0 until a > 10 loop a := a + 1 end end loop_invariant_not_maintained local a: INTEGER do from invariant a <= 0 until a > 10 loop a := a + 1 end end tagged_loop_invariant_not_maintained local a: INTEGER do from invariant tag1: a <= 0 until a > 10 loop a := a + 1 end end multi_loop_invariant_not_maintained local a, b, c: INTEGER do from invariant -- ONLY ONE ERROR REPORTED tag1: a <= 0 b <= 0 tag2: c <= 0 until a > 10 loop a := a + 1 b := b + 1 c := c + 1 end end feature -- Loop variant violation loop_variant_negative local a: INTEGER do from until a > 10 loop a := a + 1 variant a - 1 end end tagged_loop_variant_negative local a: INTEGER do from until a > 10 loop a := a + 1 variant tag1: a - 1 end end loop_variant_not_reduced local a: INTEGER do from until a > 10 loop variant 10 - a end end tagged_loop_variant_not_reduced local a: INTEGER do from until a > 10 loop variant tag1: 10 - a end end feature -- Void-call void_call_on_local: ANY local x: ANY do x.do_nothing end void_call_in_check: ANY local x: B_MESSAGES do check x.any_attribute = Void or True end end void_call_in_pre_helper (a: B_MESSAGES) note status: skip require a.any_attribute = Void do end void_call_in_pre: ANY do void_call_in_pre_helper (Void) end void_call_in_loop_inv do -- TODO end void_call_in_loop_var do -- TODO end any_attribute: ANY void_call_on_attribute: ANY do any_attribute.do_nothing end void_call_on_function do void_call_on_local.do_nothing end feature {NONE} -- Overflow overflow_in_body (a, b: INTEGER): INTEGER do Result := a + b end overflow_in_check (a, b: INTEGER): INTEGER require a > 0 and b > 0 do check a + b > 0 end end overflow_in_post (a, b: INTEGER): INTEGER require a > 0 and b > 0 do ensure a + b > 0 end overflow_in_pre_helper (a, b, c, d: INTEGER) note status: skip require tag1: a + b > 0 c + d > 0 do end overflow_in_pre (a, b: INTEGER) require a > 0 and b > 0 do overflow_in_pre_helper (1, 1, a, b) end overflow_in_pre_tagged (a, b: INTEGER) require a > 0 and b > 0 do overflow_in_pre_helper (a, b, 1, 1) end feature -- Ownership ownership_assignment_current_not_open note explicit: "all" require observers = [] modify (Current) do any_attribute := Void end ownership_assignment_heap_not_writable note explicit: "all" require observers = [] is_open modify ([]) do any_attribute := Void end ownership_assignment_observers_open_or_preserved note explicit: "all" require is_open modify (Current) do any_attribute := Void end ownership_default_wrap_fails do wrap end ownership_default_is_wrapped_violated note explicit: wrapping do unwrap end feature -- Frame violation feature -- Class invariant feature -- Validity errors not_functional1 note status: functional do end not_functional2: INTEGER note status: functional local a: INTEGER do a := 1 Result := a end call_not_functional local a: INTEGER do not_functional1 a := not_functional2 end partial_invariant_invalid require inv_only ("abc") inv_without ("abc") do end modify_field_invalid require modify_field (1, Current) modify_field (["abc", 1], Current) do end end