Proof obligations for the second method.
- The first conjunct of J holds initially:
([|(ALL (xObj::obj). ((xObj::obj) : (Object :: obj set)));
(((Thread Int Array) :: obj set) = ({null} :: obj set));
((null::obj) : (Object_alloc :: obj set));
((Thread_t::obj) : (Object_alloc :: obj set));
(comment ''unalloc_lonely'' (ALL (x::obj). (((x::obj) ~: (Object_alloc :: obj set)) --> ((ALL (z::obj) (i::int). (((arrayRead Array_arrayState z i) :: obj) ~= (x::obj))) & ((Thread_t::obj) ~= (x::obj)) & (ALL (j::int). (((arrayRead Array_arrayState x j) :: obj) = (null::obj)))))));
(comment ''static_pointsto'' ((Thread_t::obj) : (Thread :: obj set)));
(comment ''ProcedurePrecondition'' ((cardinality {tt. (((tt::obj) ~= (null::obj)) & ((tt::obj) : (Thread :: obj set)))}) <= (Thread_count::int)));
(comment ''ProcedurePrecondition'' (ALL (tt::obj). ((((tt::obj) ~= (null::obj)) & ((tt::obj) : (Thread :: obj set))) --> ((~(fieldRead (Thread_pc_bit_1 :: (obj=>bool)) tt)) & (~(fieldRead (Thread_pc_bit_0 :: (obj=>bool)) tt))))))|] ==>
(comment ''LoopInvHoldsInitially'' ((cardinality {tt. (((tt::obj) ~= (null::obj)) & ((tt::obj) : (Thread :: obj set)) & (~(fieldRead (Thread_pc_bit_1 :: (obj=>bool)) tt)) & (~(fieldRead (Thread_pc_bit_0 :: (obj=>bool)) tt)))}) <= (Thread_count::int)))).
Proven by the free cardinality-comprehension instantiation.
- The second conjunct of J holds initially:
([|(ALL (xObj::obj). ((xObj::obj) : (Object :: obj set)));
(((Thread Int Array) :: obj set) = ({null} :: obj set));
((null::obj) : (Object_alloc :: obj set));
((Thread_t::obj) : (Object_alloc :: obj set));
(comment ''unalloc_lonely'' (ALL (x::obj). (((x::obj) ~: (Object_alloc :: obj set)) --> ((ALL (z::obj) (i::int). (((arrayRead Array_arrayState z i) :: obj) ~= (x::obj))) & ((Thread_t::obj) ~= (x::obj)) & (ALL (j::int). (((arrayRead Array_arrayState x j) :: obj) = (null::obj)))))));
(comment ''static_pointsto'' ((Thread_t::obj) : (Thread :: obj set)));
(comment ''ProcedurePrecondition'' ((cardinality {tt. (((tt::obj) ~= (null::obj)) & ((tt::obj) : (Thread :: obj set)))}) <= (Thread_count::int)));
(comment ''ProcedurePrecondition'' (ALL (tt::obj). ((((tt::obj) ~= (null::obj)) & ((tt::obj) : (Thread :: obj set))) --> ((~(fieldRead (Thread_pc_bit_1 :: (obj=>bool)) tt)) & (~(fieldRead (Thread_pc_bit_0 :: (obj=>bool)) tt))))));
(comment ''LoopInvHoldsInitially'' ((tt_33::obj) ~= (null::obj)));
(comment ''LoopInvHoldsInitially'' ((tt_33::obj) : (Thread :: obj set)));
(comment ''LoopInvHoldsInitially'' (fieldRead (Thread_pc_bit_1 :: (obj=>bool)) tt_33));
(comment ''LoopInvHoldsInitially'' (~(fieldRead (Thread_pc_bit_0 :: (obj=>bool)) tt_33)))|] ==>
(comment ''LoopInvHoldsInitially'' ((Thread_count::int) = (0::int)))).
Proven by MONA.
- The first conjunct of J holds after the transition from
A to B:
([|(ALL (xObj::obj). ((xObj::obj) : (Object :: obj set)));
(((Thread Int Array) :: obj set) = ({null} :: obj set));
((null::obj) : (Object_alloc :: obj set));
((Thread_t::obj) : (Object_alloc :: obj set));
(comment ''unalloc_lonely'' (ALL (x::obj). (((x::obj) ~: (Object_alloc :: obj set)) --> ((ALL (z::obj) (i::int). (((arrayRead Array_arrayState z i) :: obj) ~= (x::obj))) & ((Thread_t::obj) ~= (x::obj)) & (ALL (j::int). (((arrayRead Array_arrayState x j) :: obj) = (null::obj)))))));
(comment ''static_pointsto'' ((Thread_t::obj) : (Thread :: obj set)));
(comment ''ProcedurePrecondition'' ((cardinality {tt. (((tt::obj) ~= (null::obj)) & ((tt::obj) : (Thread :: obj set)))}) <= (Thread_count::int)));
(comment ''ProcedurePrecondition'' (ALL (tt::obj). ((((tt::obj) ~= (null::obj)) & ((tt::obj) : (Thread :: obj set))) --> ((~(fieldRead (Thread_pc_bit_1 :: (obj=>bool)) tt)) & (~(fieldRead (Thread_pc_bit_0 :: (obj=>bool)) tt))))));
(comment ''alloc_loop_monotone'' ((Object_alloc :: obj set) ⊆ (Object_alloc :: obj set)));
(comment ''Thread.t_alloced_loop'' ((Thread_t_2::obj) : (Object_alloc :: obj set)));
(comment ''AssumingLoopInv'' ((cardinality {tt. (((tt::obj) ~= (null::obj)) & ((tt::obj) : (Thread :: obj set)) & (~(fieldRead (Thread_pc_bit_1_2 :: (obj=>bool)) tt)) & (~(fieldRead (Thread_pc_bit_0_3 :: (obj=>bool)) tt)))}) <= (Thread_count_2::int)));
(comment ''AssumingLoopInv'' (ALL (tt::obj). ((((tt::obj) ~= (null::obj)) & ((tt::obj) : (Thread :: obj set)) & (fieldRead (Thread_pc_bit_1_2 :: (obj=>bool)) tt) & (~(fieldRead (Thread_pc_bit_0_3 :: (obj=>bool)) tt))) --> ((Thread_count_2::int) = (0::int)))));
((Thread_t_1::obj) : (Thread :: obj set));
((Thread_t_1::obj) ~= (null::obj));
(comment ''TrueBranch'' ((~((fieldRead (Thread_pc_bit_1_2 :: (obj=>bool)) (Thread_t_1::obj)) :: bool)) :: bool));
(comment ''FalseBranch'' (~((fieldRead (Thread_pc_bit_0_3 :: (obj=>bool)) (Thread_t_1::obj)) :: bool)))|] ==>
(comment ''LoopInvPreserved'' ((cardinality {tt. (((tt::obj) ~= (null::obj)) & ((tt::obj) : (Thread :: obj set)) & (~(fieldRead (Thread_pc_bit_1_2 :: (obj=>bool)) tt)) & (~(fieldRead ((fieldWrite (Thread_pc_bit_0_3 :: (obj=>bool)) (Thread_t_1::obj) True) :: (obj=>bool)) tt)))}) <= (((Thread_count_2::int) - (1::int)) :: int)))).
Proven by the free cardinality-comprehension instantiation.
- The second conjunct of J holds after the transition from
A to B:
([|(ALL (xObj::obj). ((xObj::obj) : (Object :: obj set)));
(((Thread Int Array) :: obj set) = ({null} :: obj set));
((null::obj) : (Object_alloc :: obj set));
((Thread_t::obj) : (Object_alloc :: obj set));
(comment ''unalloc_lonely'' (ALL (x::obj). (((x::obj) ~: (Object_alloc :: obj set)) --> ((ALL (z::obj) (i::int). (((arrayRead Array_arrayState z i) :: obj) ~= (x::obj))) & ((Thread_t::obj) ~= (x::obj)) & (ALL (j::int). (((arrayRead Array_arrayState x j) :: obj) = (null::obj)))))));
(comment ''static_pointsto'' ((Thread_t::obj) : (Thread :: obj set)));
(comment ''ProcedurePrecondition'' ((cardinality {tt. (((tt::obj) ~= (null::obj)) & ((tt::obj) : (Thread :: obj set)))}) <= (Thread_count::int)));
(comment ''ProcedurePrecondition'' (ALL (tt::obj). ((((tt::obj) ~= (null::obj)) & ((tt::obj) : (Thread :: obj set))) --> ((~(fieldRead (Thread_pc_bit_1 :: (obj=>bool)) tt)) & (~(fieldRead (Thread_pc_bit_0 :: (obj=>bool)) tt))))));
(comment ''alloc_loop_monotone'' ((Object_alloc :: obj set) ⊆ (Object_alloc :: obj set)));
(comment ''Thread.t_alloced_loop'' ((Thread_t_2::obj) : (Object_alloc :: obj set)));
(comment ''AssumingLoopInv'' ((cardinality {tt. (((tt::obj) ~= (null::obj)) & ((tt::obj) : (Thread :: obj set)) & (~(fieldRead (Thread_pc_bit_1_2 :: (obj=>bool)) tt)) & (~(fieldRead (Thread_pc_bit_0_3 :: (obj=>bool)) tt)))}) <= (Thread_count_2::int)));
(comment ''AssumingLoopInv'' (ALL (tt::obj). ((((tt::obj) ~= (null::obj)) & ((tt::obj) : (Thread :: obj set)) & (fieldRead (Thread_pc_bit_1_2 :: (obj=>bool)) tt) & (~(fieldRead (Thread_pc_bit_0_3 :: (obj=>bool)) tt))) --> ((Thread_count_2::int) = (0::int)))));
((Thread_t_1::obj) : (Thread :: obj set));
((Thread_t_1::obj) ~= (null::obj));
(comment ''TrueBranch'' ((~((fieldRead (Thread_pc_bit_1_2 :: (obj=>bool)) (Thread_t_1::obj)) :: bool)) :: bool));
(comment ''FalseBranch'' (~((fieldRead (Thread_pc_bit_0_3 :: (obj=>bool)) (Thread_t_1::obj)) :: bool)));
(comment ''LoopInvPreserved'' ((tt_20::obj) ~= (null::obj)));
(comment ''LoopInvPreserved'' ((tt_20::obj) : (Thread :: obj set)));
(comment ''LoopInvPreserved'' (fieldRead (Thread_pc_bit_1_2 :: (obj=>bool)) tt_20));
(comment ''LoopInvPreserved'' (~(fieldRead ((fieldWrite (Thread_pc_bit_0_3 :: (obj=>bool)) (Thread_t_1::obj) True) :: (obj=>bool)) tt_20)))|] ==>
(comment ''LoopInvPreserved'' ((((Thread_count_2::int) - (1::int)) :: int) = (0::int)))).
Proven by manual but otherwise purely syntactic rewriting into SMTLIB 2.0, supplying two axioms about cardinality and running Z3. Also proven in Isabelle under a user-given general-purpose three-line-lemma.
- The first conjunct of J holds after the transition from
B to C:
([|(ALL (xObj::obj). ((xObj::obj) : (Object :: obj set)));
(((Thread Int Array) :: obj set) = ({null} :: obj set));
((null::obj) : (Object_alloc :: obj set));
((Thread_t::obj) : (Object_alloc :: obj set));
(comment ''unalloc_lonely'' (ALL (x::obj). (((x::obj) ~: (Object_alloc :: obj set)) --> ((ALL (z::obj) (i::int). (((arrayRead Array_arrayState z i) :: obj) ~= (x::obj))) & ((Thread_t::obj) ~= (x::obj)) & (ALL (j::int). (((arrayRead Array_arrayState x j) :: obj) = (null::obj)))))));
(comment ''static_pointsto'' ((Thread_t::obj) : (Thread :: obj set)));
(comment ''ProcedurePrecondition'' ((cardinality {tt. (((tt::obj) ~= (null::obj)) & ((tt::obj) : (Thread :: obj set)))}) <= (Thread_count::int)));
(comment ''ProcedurePrecondition'' (ALL (tt::obj). ((((tt::obj) ~= (null::obj)) & ((tt::obj) : (Thread :: obj set))) --> ((~(fieldRead (Thread_pc_bit_1 :: (obj=>bool)) tt)) & (~(fieldRead (Thread_pc_bit_0 :: (obj=>bool)) tt))))));
(comment ''alloc_loop_monotone'' ((Object_alloc :: obj set) ⊆ (Object_alloc :: obj set)));
(comment ''Thread.t_alloced_loop'' ((Thread_t_2::obj) : (Object_alloc :: obj set)));
(comment ''AssumingLoopInv'' ((cardinality {tt. (((tt::obj) ~= (null::obj)) & ((tt::obj) : (Thread :: obj set)) & (~(fieldRead (Thread_pc_bit_1_2 :: (obj=>bool)) tt)) & (~(fieldRead (Thread_pc_bit_0_3 :: (obj=>bool)) tt)))}) <= (Thread_count_2::int)));
(comment ''AssumingLoopInv'' (ALL (tt::obj). ((((tt::obj) ~= (null::obj)) & ((tt::obj) : (Thread :: obj set)) & (fieldRead (Thread_pc_bit_1_2 :: (obj=>bool)) tt) & (~(fieldRead (Thread_pc_bit_0_3 :: (obj=>bool)) tt))) --> ((Thread_count_2::int) = (0::int)))));
((Thread_t_1::obj) : (Thread :: obj set));
((Thread_t_1::obj) ~= (null::obj));
(comment ''TrueBranch'' ((~((fieldRead (Thread_pc_bit_1_2 :: (obj=>bool)) (Thread_t_1::obj)) :: bool)) :: bool));
(comment ''TrueBranch'' ((fieldRead (Thread_pc_bit_0_3 :: (obj=>bool)) (Thread_t_1::obj)) :: bool));
(comment ''TrueBranch'' (((Thread_count_2::int) = (0::int)) :: bool))|] ==>
(comment ''LoopInvPreserved'' ((cardinality {tt. (((tt::obj) ~= (null::obj)) & ((tt::obj) : (Thread :: obj set)) & (~(fieldRead ((fieldWrite (Thread_pc_bit_1_2 :: (obj=>bool)) (Thread_t_1::obj) True) :: (obj=>bool)) tt)) & (~(fieldRead ((fieldWrite (Thread_pc_bit_0_3 :: (obj=>bool)) (Thread_t_1::obj) False) :: (obj=>bool)) tt)))}) <= (Thread_count_2::int)))).
Proven by the free cardinality-comprehension instantiation.
-
The second conjunct of J holds after the transition from
B to C:
([|(comment ''TrueBranch'' (((Thread_count_2::int) = (0::int)) :: bool));
(comment ''TrueBranch'' ((fieldRead (Thread_pc_bit_0_3 :: (obj=>bool)) (Thread_t_1::obj)) :: bool));
(comment ''TrueBranch'' ((~((fieldRead (Thread_pc_bit_1_2 :: (obj=>bool)) (Thread_t_1::obj)) :: bool)) :: bool));
((Thread_t_1::obj) ~= (null::obj));
((Thread_t_1::obj) : (Thread :: obj set));
(comment ''AssumingLoopInv'' (ALL (tt::obj). ((((tt::obj) ~= (null::obj)) & ((tt::obj) : (Thread :: obj set)) & (fieldRead (Thread_pc_bit_1_2 :: (obj=>bool)) tt) & (~(fieldRead (Thread_pc_bit_0_3 :: (obj=>bool)) tt))) --> ((Thread_count_2::int) = (0::int)))));
(comment ''AssumingLoopInv'' ((cardinality {tt. (((tt::obj) ~= (null::obj)) & ((tt::obj) : (Thread :: obj set)) & (~(fieldRead (Thread_pc_bit_1_2 :: (obj=>bool)) tt)) & (~(fieldRead (Thread_pc_bit_0_3 :: (obj=>bool)) tt)))}) <= (Thread_count_2::int)));
(comment ''Thread.t_alloced_loop'' ((Thread_t_2::obj) : (Object_alloc :: obj set)));
(comment ''alloc_loop_monotone'' ((Object_alloc :: obj set) ⊆ (Object_alloc :: obj set)));
(comment ''ProcedurePrecondition'' (ALL (tt::obj). ((((tt::obj) ~= (null::obj)) & ((tt::obj) : (Thread :: obj set))) --> ((~(fieldRead (Thread_pc_bit_1 :: (obj=>bool)) tt)) & (~(fieldRead (Thread_pc_bit_0 :: (obj=>bool)) tt))))));
(comment ''ProcedurePrecondition'' ((cardinality {tt. (((tt::obj) ~= (null::obj)) & ((tt::obj) : (Thread :: obj set)))}) <= (Thread_count::int)));
(comment ''static_pointsto'' ((Thread_t::obj) : (Thread :: obj set)));
(comment ''unalloc_lonely'' (ALL (x::obj). (((x::obj) ~: (Object_alloc :: obj set)) --> ((ALL (z::obj) (i::int). (((arrayRead Array_arrayState z i) :: obj) ~= (x::obj))) & ((Thread_t::obj) ~= (x::obj)) & (ALL (j::int). (((arrayRead Array_arrayState x j) :: obj) = (null::obj)))))));
((Thread_t::obj) : (Object_alloc :: obj set));
((null::obj) : (Object_alloc :: obj set));
(((Thread Int Array) :: obj set) = ({null} :: obj set));
(ALL (xObj::obj). ((xObj::obj) : (Object :: obj set)))|] ==>
(ALL (tt::obj). ((((tt::obj) ~= (null::obj)) & ((tt::obj) : (Thread :: obj set)) & (fieldRead ((fieldWrite (Thread_pc_bit_1_2 :: (obj=>bool)) (Thread_t_1::obj) True) :: (obj=>bool)) tt) & (~(fieldRead ((fieldWrite (Thread_pc_bit_0_3 :: (obj=>bool)) (Thread_t_1::obj) False) :: (obj=>bool)) tt))) --> ((Thread_count_2::int) = (0::int))))).
Proven internally.