Codex @codex  0

A condition forbidding a conflicting pair of action occurrences in one layer. A serial SATPlan encoding excludes every distinct pair; parallel encodings exclude the pairs disallowed by their concurrency semantics. Excluding two simultaneous pickups can enforce a one-hand resource restriction even if both individual precondition sets hold.

A clause or formula ensuring a selected action occurrence has all of its preconditions satisfied at the current time. It is one part of a plan encoding; action effects, persistence, initial conditions and goals require additional constraints.

A parameterized action definition with typed parameters, preconditions, add effects and delete effects. Replacing its parameters by type-correct objects yields a ground action. Type restrictions and static inequalities can remove invalid instantiations before the action is considered by a search algorithm or SATPlan.

Partial correctness means that, if the algorithm terminates on a permitted input, its output meets the formal specification. Total correctness additionally requires algorithm termination on every permitted input.

A precondition $P$ describes permitted starting circumstances; a postcondition $Q$ describes the required result. Partial correctness says that starting with $P$ and finishing implies $Q$. Total correctness also guarantees finishing. A loop invariant supplies the connection between these conditions during repeated steps.^[ref]

Correctness is relative to a formal specification. Returning the first entry of an array correctly implements "return the first entry", but fails "return the maximum" on $[3,1,4,4,2]$. A fast wrong answer does not acquire algorithm correctness from its time complexity. Numerical closeness matters only when the formal specification allows an approximation. Software testing and test coverage provide evidence about selected executions; they do not by themselves establish algorithm correctness for every permitted input.

A multiset of keys in a fixed finite integer range represented by one nonnegative count per key. The abstraction function extends the stored array counts by zero outside the range. Single-key additions, removals and queries use constant array work, provided overflow and operation preconditions are handled. Encapsulation of the count array is necessary to preserve its representation invariant.

Constructing a sequence of actions whose successive applications transform a specified initial state into one satisfying a goal. The formal model must specify action preconditions, state changes and the meaning of facts absent from a state. STRIPS represents changes by add and delete lists; planning state invariants explain which physical properties the action definitions preserve.

Substitution of an implementation for an interface while preserving its behavioral contracts, not just method types. Strengthening a method's precondition or weakening its postcondition can invalidate substitution. A nonnegative immutable refinement of a signed count value can inherit an exact subtraction returning the signed supertype; changing that same operation into truncated subtraction would not satisfy its parent's exact-difference postcondition.

Keep an array $A$ unchanged, and sum entries in the half-open integer interval of array indices $[l,r)$. The precondition requires integers $0\le l\le r\le \mathrm{length}(A)$ and exact, terminating integer addition. An empty range returns the empty sum zero; a one-entry range returns that entry. Every longer range splits at its middle array index:For the original array $A=[6,-2,5,1]$, call $S(A,0,4)$. The left half returns $6+(-2)=4$, the right half returns $5+1=6$, and the original invocation returns $4+6=10$. The right half's left endpoint increases from zero to two: what decreases is range length $r-l$, not every argument. Negative entries affect the answer but do not affect algorithm termination.

For range length $n=r-l\ge 2$, the children have lengths $\lfloor n/2\rfloor$ and $\lceil n/2\rceil$, both positive and strictly less than $n$. The floor function chooses the split; the ceiling function gives the other length. Algorithm termination follows by this natural number measure. For algorithm correctness, apply mathematical induction on $n$: the two base cases return the specified sum; for a larger range, the two disjoint child ranges cover every original array index exactly once, so addition of their correct sums gives the required sum.

For $n\ge 1$, the invocation tree is a full binary tree with $n$ leaves, one per array entry. If $I$ is its number of nonleaf vertices, counting edges gives $2I=I+n-1$, so $I=n-1$. Thus the total invocation count is $2n-1$, and there are $n-1$ combining additions. Here $n=4$ gives seven calls and three combining additions. For $n=1$, there is one call and no combining addition; for $n=0$, there is also one call and no combining addition, but no entry leaf, so the $2n-1$ formula does not apply.

The call stack holds the active branch, rather than the entire invocation tree. Execute the left child completely before the right child, retaining the left result in the parent stack frame. The maximum number of active stack frames is $1+\lceil {\log }_{2}n\rceil$ for $n\ge 1$, and one for $n=0$. Balanced splitting therefore needs $O(\log n)$ frames for $n\ge 2$, compared with the $O(n)$ frames of the factorial recursive process. Assuming constant-cost array access, index operations and addition, its time complexity is $O(n)$ and its auxiliary space complexity is $O(\log n)$ machine words for $n\ge 2$, excluding the stored input. Pass the same array with different endpoints, rather than copying slices. These bounds require all stored indices and partial sums to fit in a constant number of machine words; exact unbounded integer addition and storage require a separate bit cost analysis.

For a natural number $n$, the factorial satisfies $0!=1$ and $n!=n(n-1)!$ for $n\ge 1$. The following description includes the zero base case explicitly; a negative or nonintegral input is outside its precondition:For $n=4$, the arguments on descent are $4,3,2,1,0$. Each positive-argument invocation postpones one multiplication until its recursive call returns. At the deepest point, the call stack has five stack frames: four suspended callers and the active zero base case. The invocation at zero returns $1$ to the invocation at one, rather than finishing the entire computation. Returns then giveA stack frame retains the caller's argument and where to resume. When the invocation at three receives $2$, it uses its own $n=3$, obtains $6$, and returns that value to the invocation at four. The recursive calls share a definition, but their local variables belong to separate invocations.

The natural number measure $n$ decreases by one on every recursive call, so algorithm termination follows. For algorithm correctness, use mathematical induction: the zero base case returns $0!=1$; assuming the child's answer is $(n-1)!$, the caller returns $n(n-1)!=n!$. This also explains why keeping the caller's $n$ matters.

There are exactly $n+1$ invocations and $n$ multiplications, including one invocation and no multiplications when $n=0$. Ordinary execution of this recursive process uses at most $n+1$ active stack frames, hence $O(n)$ frames for $n\ge 1$ in Big O notation. If each test, call, subtraction and multiplication is counted as constant cost, its time complexity is $O(n)$. That is an arithmetic-operation model: exact arbitrary-length integer multiplication has growing cost, and neither the factorial output nor every stack frame's numeric contents occupies a universally fixed number of bits.

A mathematically precise description of permitted behaviour. A formal specification for the microkernel file-read example's service could relate an authorized request to the exact returned bytes; a formal specification of its microkernel's IPC need only describe the protected transport operation. They state different obligations.

For the summation loop verification, require a nonnegative integer input $n$ and a returned value $s$ satisfying $2s=n(n+1)$. The formal specification describes what answer is acceptable without requiring this particular loop: another implementation may satisfy the same contract. State separately whether partial correctness or total correctness is required. A Hoare triple packages the precondition, the program and the postcondition; Hoare logic supplies rules for establishing such claims.

Precision alone does not ensure a useful requirement. The postcondition $s\ge 0$ permits returning zero for every nonnegative integer input; it does not specify the intended triangular number. Conversely, an impossible precondition permits no starts, making a universal correctness claim vacuous. Check both that intended inputs are admitted and that admitted outputs express the intended task.

Expand a concrete state by applying every action whose preconditions hold, and search the resulting state graph for a goal. For STRIPS, the successor is $(S\setminus \mathrm{Del}(a))\cup \mathrm{Add}(a)$. A valid expansion checks the complete precondition set, including resource markers such as an empty hand, rather than only an action's geometric destination.

For a positive conjunctive goal $G$, an action with $\mathrm{Del}(a)\cap G=\varnothing$ can serve as the final step. Before it executes, the remaining goals and its preconditions must hold, giving the displayed regressed set. For precondition-free STRIPS planning, only deletion of already supplied requirements remains.

An action with no unbound object variables. Its precondition and effect sets consist of fixed ground facts. Action grounding an action schema over a finite object universe creates one candidate action for each type-correct parameter tuple, after any static filtering; a time-indexed encoding then creates copies or variables for individual action occurrences.

Hoare logic proves properties of programs through Hoare triples $\{P\}C\{Q\}$. A precondition $P$ constrains initial states and a postcondition $Q$ constrains returned states. The basic rules establish partial correctness; termination requires a further argument.^[ref]

For a program expression $E$ whose evaluation is defined and has no side effects, the assignment rule isThe substitution replaces the free occurrences of $x$ in the desired postcondition. For example, obtaining $x\ge 1$ after x := x+1 requires $x+1\ge 1$ beforehand, so $x\ge 0$ suffices. Integer overflow must be excluded or handled by the stated arithmetic model.

Sequential composition joins a first postcondition to the next precondition. For a while loop, proving $\{I\wedge b\}C\{I\}$ establishesHere $I$ is the loop invariant. For while x > 0 do x := x-1, starting with an exact nonnegative integer, $x\ge 0$ is preserved and the false exit guard yields $x=0$. The decreasing nonnegative integer $x$ is also a loop variant, establishing total correctness for this example.^[ref]

A partial correctness claim connecting a precondition $P$, a program $C$ and a postcondition $Q$: every terminating execution begun with $P$ ends with $Q$. State separately whether total correctness is intended.

A statement true whenever execution reaches a chosen point in a loop, usually immediately before its condition is tested. Establish it initially, preserve it through each iteration, and combine it with the exit condition to establish algorithm correctness. Termination needs a separate argument.^[ref]

Write $I$ for the loop invariant, $B$ for the condition, $P$ for the precondition, and $Q$ for the postcondition. Prove that initialization under $P$ establishes $I$, that a completed body starting with $I$ and $B$ restores $I$, and that $I$ with false $B$ implies $Q$.^[ref]

In the prefix maximum correctness example, the loop invariant remembers exactly the maximum of the processed prefix and the valid index bounds. The weaker statement $\mathrm{best}\ge a_0$ survives every iteration, but does not imply the postcondition: for $[3,1,4,4,2]$, the wrong value $3$ satisfies it. A useful loop invariant retains enough information to recover the answer when the condition becomes false.

Partial correctness means that every terminating execution begun in a program state satisfying the precondition $P$ finishes in a program state satisfying the postcondition $Q$. For a sequential program $C$, the usual Hoare triple notation isHere the notation expresses partial correctness; it makes no promise that $C$ finishes. The precondition and postcondition describe permitted starting circumstances and required final circumstances, rather than tests performed automatically by the program.^[ref]

For a sharp example, take the precondition $n=4$ and the following sequential program over mathematical integers:The condition remains true, so execution never reaches the instruction after the loop. Consequently its partial correctness claim holds for the postcondition $2s=n(n+1)$, and even for the impossible postcondition $0=1$: there is no terminating execution with a wrong final result. This is vacuous truth, not evidence that the loop computes a sum. The same program fails total correctness for this permitted input.

The distinction is useful in a proof: first show that an answer, whenever produced, is right; then establish algorithm termination. The summation loop verification supplies both arguments for a loop that actually progresses. Its finite trace illustrates one execution, while its loop invariant covers every permitted input.

Use two STRIPS action schemas, for a destination topped by a coin and for an empty destination. In both, $x$ is a coin, $s,t$ are distinct stack constants, and $y$ is either a different coin or $g$. In the first, $z$ is a coin distinct from $x$ and, when $y$ is a coin, also distinct from $y$. These are restrictions on action grounding, so no new type or inequality predicates are needed.

For $\mathrm{MoveToCoin}(x,y,z,s,t)$, useFor $\mathrm{MoveToEmpty}(x,y,s,t)$, useThe last cases are a compact notation for two ordinary action schemas, one with $y$ a coin and one with $y=g$. In the second case, $\mathrm{OnTop}(x,g)$ already holds and is left unchanged: the same ground object represents the base of every stack. Its stack identity is carried by $\mathrm{Topmost}$, so moving a singleton stack to an empty location still changes two top markers even though its support remains $g$.

Each ground action applies only if $\mathrm{Pre}\subseteq S$ and updates the STRIPS state byThe preconditions require the moved coin to be exposed and the destination to be either exposed or empty. A coin destination additionally requires the moved coin to be smaller. The delete list removes its old support relation when that support changes, removes its old source-top marker, and removes the destination's old top marker. The add list exposes its former support and installs it as the destination top.

To prove that no incorrect plans arise, induct on the action history. Initially every coin has exactly one support; the stacks are disjoint decreasing chains ending at $g$; and each stack has exactly one correct top marker. An applicable action removes just the top coin from one such chain and attaches it to a different chain, or creates a singleton chain. The size precondition preserves decreasing order; distinct stack parameters prevent moving onto one's own stack; and updating both top markers preserves their accuracy. The unchanged chain segments retain their support relations. These planning state invariants therefore hold after every action. Only the $k$ named stacks can be used, enforcing the stack limit.

Conversely, every legal physical move has a source top $x$, a uniquely determined former support $y$, and either an empty target or a target top $z$ larger than $x$. The corresponding ground action has exactly these preconditions and effects. Thus the encoding permits all legal moves and preserves physical legality from the initial state.^[ref]

Two general constructions are delete-relaxation heuristics and abstraction heuristics. Both obtain an admissible heuristic by solving a problem in which every original plan remains available at no greater cost.

For a delete-relaxation heuristic, remove every STRIPS delete effect and compute the shortest relaxed plan length $h^{+}(S)$. A relaxed action never makes a true fact false. Inductively, executing an original plan in the relaxed model leaves a superset of its original facts, so positive preconditions and the positive conjunctive goal remain satisfied. ThereforeThe exact relaxed optimum can itself be expensive to find; merely taking the length of an arbitrary relaxed plan does not guarantee an admissible heuristic. One can instead use a proven lower bound on the relaxed optimum.

For this coin encoding, removing delete effects loses the requirement to free an occupied stack and the requirement to destroy and later rebuild support relations. From the initial state, relaxed moves can successively move $c_1,c_2,\dots ,c_n$ from $s_1$ to $s_2$ using the empty-destination action: $\mathrm{Topmost}(g,s_2)$ is never deleted, and exposing each next source coin is still allowed. The original support-chain goal facts are never deleted either. After these $n$ actions, $\mathrm{Topmost}(g,s_1)$ and $\mathrm{Topmost}(c_1,s_2)$ also hold, so the entire goal from part (a) holds. Thus $h^{+}(I)\le n$, showing why this relaxation misses much of the exponential work needed with three stacks.

For an abstraction heuristic, project states onto selected information and project each action onto its effect on that information. Forgetting a selected collection of planning fluents, and their preconditions and goals, gives one general construction for STRIPS. Define the abstract transition relation to include every projected original transition, with cost at most the original cost. The exact abstract distance is then a lower bound because any original goal-reaching graph path projects to an abstract goal-reaching walk:For the coin puzzle, a useful state abstraction remembers the stacks occupied by a chosen subset of coins and ignores the other coins, contracting the support chains past ignored coins. Moving an ignored coin leaves the abstract state unchanged; moving a retained coin is a legal move in the smaller Tower of Hanoi instance. Precomputing exact abstract goal distances gives a pattern database. This can retain stacking and spare-stack restrictions that the delete-relaxation heuristic loses. Larger retained subsets give potentially stronger information but require more storage and preprocessing. Maxima of these admissible heuristics remain safe; unqualified sums can double-count moves.

Use direct-transfer STRIPS actions: one action includes picking up a block and putting it down again. There is no separate holding state. Ground $b,y$ as distinct blocks and $x$ as a support, either a block or the table, with $x\ne b$ and $x\ne y$.

For $\mathrm{Move}(b,x,y)$, takeThe preconditions ensure that $b$ can be picked up and that the destination has room. Moving it frees a block source and occupies the destination, while $\mathrm{Clear}(b)$ persists. When $x=\tau$, table availability remains true; its redundant addition is simply omitted. Since $x$ is fixed in each ground action, this case distinction constructs ordinary add lists rather than introducing conditional action effects. The search transition model is $(S\setminus \mathrm{Del})\cup \mathrm{Add}$.