Separation logic: improve documentation.

Author: kfriedberger

src/org/sosy_lab/java_smt/api/SLFormulaManager.java

@@ -2,7 +2,7 @@
 // an API wrapper for a collection of SMT solvers:
 // https://github.com/sosy-lab/java-smt
 //
-// SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+// SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
@@ -15,18 +15,73 @@
  * all formulae for one heap need to use matching types (sorts) for the AdressFormulae and
  * ValueFormulae. The user has to take care of this, otherwise the {@link ProverEnvironment}
  * complains at runtime!
+ *
+ * @see <a href="https://en.wikipedia.org/wiki/Separation_logic">Separation Logic</a>
+ * @see <a href="https://cacm.acm.org/research/separation-logic/>Separation Logic</a>
+ * @see <a
+ *     href="https://www.cs.cmu.edu/afs/cs.cmu.edu/project/fox-19/member/jcr/www15818As2011/cs818A3-11.html">15-818A3
+ *     Introduction to Separation Logic (6 units) Spring 2011</a>
+ * @see <a href="https://www.philipzucker.com/executable-seperation>Modeling Separation Logic with
+ *     Python Dicts and Z3</a>
  */
 @SuppressWarnings("MethodTypeParameterName")
 public interface SLFormulaManager {
 
+  /**
+   * Creates a formula representing the "separating conjunction" (*) of two Boolean formulas. In
+   * separation logic, the separating conjunction asserts that the two formulas describe disjoint
+   * parts of the heap. It is similar to the logical AND operator, but with the additional
+   * constraint that the memory regions described by the two formulas do not overlap.
+   *
+   * @return a Boolean formula representing the separating conjunction of {@code f1} and {@code f2}.
+   */
   BooleanFormula makeStar(BooleanFormula f1, BooleanFormula f2);
 
+  /**
+   * Creates a formula representing a "points-to" relation in the heap. The "points-to" relation
+   * asserts that a pointer points to a specific value in memory.
+   *
+   * @param <AF> the type of the address formula.
+   * @param <VF> the type of the value formula.
+   * @param ptr the pointer formula.
+   * @param to the value formula.
+   * @return a Boolean formula representing the "points-to" relation.
+   */
   <AF extends Formula, VF extends Formula> BooleanFormula makePointsTo(AF ptr, VF to);
 
+  /**
+   * Creates a formula representing the "magic wand" (-*) operator in separation logic. The "magic
+   * wand" operator asserts that if the first formula holds, then the second formula can be added to
+   * the heap without conflict. It is a form of implication (=>) that takes into account the
+   * disjointness of memory regions.
+   *
+   * @return a Boolean formula representing the "magic wand" of {@code f1} and {@code f2}.
+   */
   BooleanFormula makeMagicWand(BooleanFormula f1, BooleanFormula f2);
 
+  /**
+   * Creates a formula representing an empty heap. The empty heap formula asserts that no memory is
+   * allocated for the given address and value types.
+   *
+   * @param <AF> the type of the address formula.
+   * @param <VF> the type of the value formula.
+   * @param <AT> the type of the address formula type.
+   * @param <VT> the type of the value formula type.
+   * @param pAddressType the type of the address formula.
+   * @param pValueType the type of the value formula.
+   * @return a Boolean formula representing an empty heap.
+   */
   <AF extends Formula, VF extends Formula, AT extends FormulaType<AF>, VT extends FormulaType<VF>>
-      BooleanFormula makeEmptyHeap(AT pAdressType, VT pValueType);
+      BooleanFormula makeEmptyHeap(AT pAddressType, VT pValueType);
 
+  /**
+   * Creates a formula representing the "nil" element for a given address type. The "nil" element is
+   * used to represent a null pointer or an unallocated memory address.
+   *
+   * @param <AF> the type of the address formula.
+   * @param <AT> the type of the address formula type.
+   * @param pAdressType the type of the address formula.
+   * @return a formula representing the "nil" element for the given address type.
+   */
   <AF extends Formula, AT extends FormulaType<AF>> AF makeNilElement(AT pAdressType);
 }