Proof step 1 from proof alloc (conclusion) (back to tree)

Heuristic weak unfold applied rule call right

And obtained the following new goals

• Proof step 2:

  hP(h) ⊦ ⟪choose r0 with ¬ r0 ∈ h ∧ r0 ≠ null in r := r0, h := h ++ r0⟫ ((r =>_ * hP))(h)

Rule argument

Additional information

Used simplifier rules: alloc(; r, h){choose r0 with ¬ r0 ∈ h ∧ r0 ≠ null in r := r0, h := h ++ r0};

Proof step 2 from proof alloc (previous step) (back to tree)

Heuristic symbolic execution applied rule choose right

And obtained the following new goals

• Proof step 3:

  r0 ≠ null, hP(h), ¬ r0 ∈ h ⊦ ⟪r := r0, h := h ++ r0⟫ ((r =>_ * hP))(h)

• Proof step 4:

  hP(h), ∀ r0. ¬(¬ r0 ∈ h ∧ r0 ≠ null) ⊦ ⟪abort⟫ ((r =>_ * hP))(h)

Rule argument

Additional information

Proof step 3 from proof alloc (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ¬ r ∈ h, r ≠ null ⊦ ((r =>_ * hP))(h ++ r) ↔ hP(h); (ss) sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep

Proof step 4 from proof alloc (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 5:

  ⊦ ∃ r. ¬ r ∈ h ∧ r ≠ null

• Proof step 6:

  hP(h), ∀ r0. ¬(¬ r0 ∈ h ∧ r0 ≠ null), ∃ r. ¬ r ∈ h ∧ r ≠ null ⊦ ⟪abort⟫ ((r =>_ * hP))(h)

Rule argument

Additional information

Used terms: h

Proof step 5 from proof alloc (previous step) (back to tree)

A spec-lemma

Proof step 6 from proof alloc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  r0 ≠ null, hP(h), ¬ r0 ∈ h, ∀ r1. r1 ∈ h ∨ r1 = null ⊦ ⟪abort⟫ ((r =>_ * hP))(h)

Rule argument

Additional information

Proof step 7 from proof alloc (previous step) (back to tree)

Heuristic symbolic execution applied rule abort right

And obtained the following new goals

• Proof step 8:

  r0 ≠ null, hP(h), ¬ r0 ∈ h, ∀ r1. r1 ∈ h ∨ r1 = null ⊦

Rule argument

Additional information

Proof step 8 from proof alloc (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r0