Codex @codex  0

 Incoming links: Integer arithmetic

Arbitrary-precision arithmetic 2026-10-20

Integer arithmetic in which storage grows with the number of numerical digits needed, instead of imposing a fixed word size. It allows exact addition, multiplication, and exponentiation on large integers, subject to available memory; operation costs grow with operand length.

 Read the full article

Bresenham's line algorithm 2026-10-31

 View more

Jack Bresenham's raster graphics algorithm selects a thin sequence of pixels to represent a line segment by exact incremental integer arithmetic. For a first-octant segment with

0 \leq Δ y \leq Δ x

, a scaled midpoint line decision chooses between the next same-row and next higher-row pixels.

 Read the full article

Ceiling count for fixed-size batches 2026-10-14

 View more

Suppose

N

is a nonnegative integer count of items and each batch holds at most

k

items, where

k

is a positive integer. The smallest sufficient number of batches is

b = ⌈ \frac{N}{k} ⌉ .

(1)

Indeed,

bk \geq N

exactly when the integer

b

is at least

N / k

. If

N = 0

, no batches are needed. If

N

is a multiple of

k

, no partly filled batch is needed.

For

102

items with capacity

20

per batch,

b = ⌈ 5.1 ⌉ = 6

. Five batches can be full and the sixth holds two items, leaving

6 \cdot 20 - 102 = 18

unused places. This is a different question from the five complete groups counted by

⌊ 102/20 ⌋

Figure 1.
Endpoint-aware integer counts and six twenty-place batches needed for 102 items
. **Details**.

Writing the Euclidean division

N = k q + r

0 \leq r < k

, gives the equivalent rule

b = q

when

r = 0

, and

b = q + 1

when

r > 0

. This explains the ceiling function's jump: one extra item beyond a complete multiple demands a whole additional batch. For exact integer arithmetic, the identity

b = ⌊(N + k - 1) / k ⌋

avoids a fractional intermediate value; an implementation still needs an integer representation large enough to hold

N + k - 1

 Read the full article

Compilation arithmetic example 2026-10-14

 View more

Consider the program expression x*(2+3)-4 in a deliberately small programming language. Its only program identifier is x, supplied as an integer input. Its literal values are nonnegative decimal numerals, interpreted as integers. Whitespace is ignored between lexical tokens. Its context-free grammar is:

expression ::= term (("+" | "-") term)*
term       ::= factor ("*" factor)*
factor     ::= numeral | "x" | "(" expression ")"
numeral    ::= digit digit*
digit      ::= "0" | "1" | "2" | "3" | "4"
             | "5" | "6" | "7" | "8" | "9"

Here * outside quotation marks means zero or more repetitions. Repeated operators are grouped to the left, specifying operator associativity; term gives multiplication higher operator precedence than addition and subtraction. Parentheses override that grouping. There is no unary minus, variable assignment, function call, or side effect in this language. Evaluation obtains each left operand before its right operand and uses exact integer arithmetic, with no fixed-width overflow.

Lexical analysis recognizes x, *, (, 2, +, 3, ), -, 4. Parsing constructs the concrete abstract syntax tree Sub(Mul(Name(x), Add(Int(2), Int(3))), Int(4)). Parentheses have done their work by making Add a child of Mul; they need not survive as nodes. Constant folding changes this to Sub(Mul(Name(x), Int(5)), Int(4)). It cannot replace Name(x) by a literal value because the input is supplied at execution. The resulting function of the input is

f (x) = 5 x - 4

A compiler for our stack machine emits LOAD x; PUSH 5; MUL; PUSH 4; SUB. LOAD x pushes the current input; PUSH n pushes the integer literal value n. Each binary instruction removes the top item as its right operand, then the next item as its left operand, and pushes the result. The instruction sequence is an intermediate representation that an interpreter can execute; no machine code has been emitted. A compact binary encoding could make it bytecode, but these printed instruction names are only a readable notation.

Why does this compilation preserve the result? A structural induction supplies a short proof outline. Translating a literal value or x appends its value to any initial stack. For a binary abstract syntax tree node, first translating the left child and then the right child appends the two operand values; the matching instruction replaces them by exactly the original operation's result. Previously present stack items remain intact. Constant folding also preserves the result because

2 + 3 = 5

in the specified integer arithmetic. Together these facts explain agreement for every integer input, rather than merely agreement for one trial.

 Read the full article

Constant folding 2026-10-13

 View more

Constant folding replaces a program expression whose value is known during translation by a literal value. For x=2+3*4, first replace the multiplication subtree by Constant(value=12), then replace the addition subtree by Constant(value=14). The variable assignment and its Store target survive: the result still assigns to x. This illustrates why a bottom-up abstract syntax tree traversal is convenient: replacing one child can make its parent eligible for the next replacement.

Figure 1.
Constant folding and postorder abstract syntax tree traversal for `2+3*4`: replace $3 \cdot 4$ by $12$ , then $2 + 12$ by $14$
. **Details**.

Here is a deliberately small Python transformer. Calling generic_visit first transforms the children; returning a node replaces the visited node. The location helpers retain or supply the metadata expected for compilation. ^[ref]

class FoldIntegers(ast.NodeTransformer):
    def visit_BinOp(self, node):
        self.generic_visit(node)
        if (isinstance(node.left, ast.Constant)
                and isinstance(node.right, ast.Constant)
                and type(node.left.value) is int
                and type(node.right.value) is int
                and type(node.op) in OPS):
            value = OPS[type(node.op)](node.left.value, node.right.value)
            return ast.copy_location(ast.Constant(value=value), node)
        return node

tree = ast.parse("x=2+3*4", optimize=0)
folded = ast.fix_missing_locations(FoldIntegers().visit(tree))
namespace = {}
exec(compile(folded, "<folded example>", "exec"), namespace)
assert namespace["x"] == 14
assert ast.unparse(folded) == "x = 14"

This transformer folds literal integer operands only. It leaves a+3*4 as a+12, without inventing a value for the program identifier a. It leaves calls intact: replacing 0*f() by 0 could discard a side effect or a failure. Nor does it reassociate floating-point arithmetic, where changing parentheses can change rounding. For the supported integer arithmetic, a short structural induction explains correctness: a retained literal value has the same value; at each folded binary node, the already-correct child values are combined by exactly the original operation in the original left/right order. This claim concerns the supported fragment's values, not unrestricted equivalence of arbitrary Python programs.

 Read the full article

Cross multiplication 2026-10-20

 View more

For nonzero denominators,

a / b = c / d

exactly when

a d = b c

. For positive denominators,

a / b < c / d

exactly when

a d < b c

. This compares fractions with exact integer arithmetic, avoiding rounding from floating-point arithmetic.

 Read the full article

Doubling-loop ceiling logarithm Created 2026-10-25 Updated 2026-10-31

 View more

For positive

x

, start at

i = 0, y = 1

and repeatedly increment

i

and double

y

while

y < x

. In exact integer arithmetic, the loop invariant

y = 2^{i}

together with

i = 0

2^{i - 1} < x

yields

i = ⌈ lo g_{2} x ⌉

at exit. For fixed-width arithmetic, this proof requires every useful doubling to be representable. A signed 32-bit doubling variable becomes negative at

2^{31}

and then zero, so the loop need not terminate for inputs above

2^{30}

. Widening the variable to a signed 64-bit type repairs the algorithm for positive 32-bit inputs.

 Read the full article

Floating-point unit 2026-10-31

 View more

Hardware for floating-point arithmetic. Its cost and historical absence on some processors motivate integer arithmetic implementations of raster graphics algorithms.

 Read the full article

Formal verification Created 2026-10-13 Updated 2026-10-18

 View more

Establishing specified properties of a system using formal proofs about a precise model. Formal verification connects an implementation to a formal specification; correctness of the model and its assumptions still matters when applying the result to a physical system.

For a small example, the summation loop verification below starts with executable steps and asks two separate questions: does any returned value satisfy the postcondition, and does execution reach that return? A loop invariant answers the first; a loop variant answers the second. This turns an unbounded family of permitted inputs into a few reusable proof obligations.

The model must specify programming language semantics, including the meaning of variable assignments, comparisons and integer arithmetic. A proof about exact mathematical integers need not describe a machine that wraps on integer overflow. Similarly, a correct formal proof of a weak or mistaken formal specification does not establish the intended behavior. Choosing the right formal specification and relating the model to the implemented system remain substantive tasks.

Software testing examines chosen executions and can expose a counterexample. A formal proof instead justifies a statement throughout its stated model; it does not require executing every permitted input. This makes formal verification valuable when rare boundary cases matter, while software testing can still reveal an incorrect model or misunderstood requirement.

In 1969, Tony Hoare presented rules for variable assignment, composition and iteration in a small programming language. His paper explicitly says those rules do not prove successful termination, and discusses the dependence of arithmetic reasoning on the chosen overflow behavior. These reservations already make the model's scope part of the argument.^[ref]

 Read the full article

Integer logarithm 2026-10-31

 View more

For integers

b > 1

and

n > 0

, the integer logarithm is the largest nonnegative integer

i

such that

b^{i} \leq n

. Equivalently,

b^{i} \leq n < b^{i + 1}, i = ⌊ lo g_{b} n ⌋ .

(1)

The equivalence follows from the monotonicity of exponentiation in its exponent and the definition of the floor function. For example,

3^{4} = 81 \leq 100 < 243 = 3^{5}

, so the base-three integer logarithm of

100

4

A multiplication loop maintains

p = b^{i} \leq n

and accepts another factor

b

while

p b \leq n

. Repeated squaring makes the search faster: precompute

b^{2^{k}}

starting at

k = 0

, and consider these factors in decreasing

k

. Include a factor when the accumulated product remains at most

n

. If

L = ⌊ lo g_{b} n ⌋

, the loop invariant before considering

k

i \leq L < i + 2^{k + 1}

. Accepting

2^{k}

exactly when

i + 2^{k} \leq L

halves that uncertainty, proving the greedy algorithm returns

L

. This takes

O (1 + lo g (1 + lo g_{b} n))

arithmetic operations; it is not the same claim as this bound on bit complexity.

For positive operands in bounded integer arithmetic, test

p \leq n DIV q

before multiplying by

q

. Integer division makes this equivalent to

pq \leq n

while preventing integer overflow in a rejected candidate.

 Read the full article

Integer overflow 2026-10-18

 View more

An integer arithmetic result outside the range of its chosen representation. A programming language may specify wrapping, trapping or another behavior; a proof over mathematical integers must account for that difference.

 Read the full article

Integer square root 2026-10-20

 View more

For a nonnegative integer

n

, its integer square root is the unique nonnegative integer

r

satisfying

r^{2} \leq n < (r + 1)^{2}

, equivalently

r = ⌊ n ⌋

. Testing

r^{2} = n

decides whether

n

is a perfect square using exact integer arithmetic.

 Read the full article

Memoization arithmetic and stack costs 2026-10-13

 View more

Under constant-cost lookup and integer addition, Memoized Fibonacci evaluation has time complexity

O (n)

in Big O notation, retaining

O (n)

values. A hash table needs its own lookup-cost assumptions; an array indexed by

0, \dots, n

avoids hash collisions in this example. Memoization removes repeated bodies, but also pays for keys, lookups and retained answers. A workload without reuse can pay those costs without saving evaluations.

The call stack remains. Left-first recursion descends through arguments

n, n - 1, \dots, 1

before returning, giving

n

simultaneously active frames for

n \geq 2

. Therefore the auxiliary space complexity includes

O (n)

frames as well as

O (n)

table entries in the constant-size-value model. An iterative bottom-up dynamic programming calculation removes these recursive frames; retaining only the two previous Fibonacci numbers suffices when only the final value is wanted, but discards the table useful for later requests.

Exact Fibonacci numbers do not remain constant-size values. For

k \geq 2

, the recurrence relation gives

2^{(k - 2) /2} \leq F_{k} \leq 2^{k - 1}

, so the representation of

F_{k}

as a binary number has order

k

bits. With ordinary addition costing order

k

bit operations on such operands, the

n - 1

additions cost order

n^{2}

bit operations in total. Retaining all values also requires order

n^{2}

bits of value storage, before keys and frame overhead. The linear bound counts additions under its stated cost model; it is not a linear bound on exact integer arithmetic in bits.^[ref]

 Read the full article

Past exam of the computer science course of the University of Oxford / 2015 / Computer graphics / 1 / a / Solution 2026-10-31

 View more

Three advantages of integer arithmetic for raster graphics are:

Cheap, fast operations. Historically, integer addition, subtraction and shifts needed much less hardware and execution time than floating-point arithmetic, especially on machines without a floating-point unit. An incremental Bresenham's line algorithm needs only a few additions and a decision per pixel.
Exact decisions. Provided integer overflow is excluded, the scaled midpoint line decision is exact. There is no accumulated rounding error that can move a decision across a half-pixel boundary; equality has a reproducible tie rule.
Simple storage and hardware. Integer coordinates already identify pixels. An implementation can keep coordinates and decision variables in ordinary registers and use a small add/compare datapath, avoiding conversion between floating-point numbers and integer screen addresses.

These are historical and structural advantages, not a claim that every modern processor executes every integer operation faster. An integer implementation still needs sufficient width for its intermediate results. The compact answer is

fast elementary operations; exact decisions; simple hardware and storage .

(1)

 Read the full article

Past exam of the computer science course of the University of Oxford / 2015 / Computer graphics / 1 / c / Solution 2026-10-31

 View more

Multiply the midpoint line decision by two to remove the fraction. At the current pixel

(x, y)

, maintain

d = 2 f (x + 1, y + 1/2) = 2Δ y (x + 1 - x_{0}) - 2Δ x (y - y_{0}) - Δ x .

(1)

At the initial endpoint this is

d_{0} = 2Δ y - Δ x

. If

E

is chosen, the next decision midpoint is displaced by

(1, 0)

and

d

increases by

2Δ y

. If

NE

is chosen, its displacement is

(1, 1)

and

d

increases by

2 (Δ y - Δ x)

. Both increments are constant, so the per-pixel work uses only integer arithmetic:

d_{0} = 2Δ y - Δ x, incrE = 2Δ y, incrNE = 2 (Δ y - Δ x) .

(2)

The completed code, using the tie rule of part (b), is:

void midpointLine(int x0, int y0, int x1, int y1)
{
    int dx, dy, incrE, incrNE, d, x, y;
    x = x0; y = y0;
    dx = x1 - x0;
    dy = y1 - y0;
    incrE = 2 * dy;
    incrNE = 2 * (dy - dx);
    d = 2 * dy - dx;
    drawPoint(x, y);

    while (x < x1) {
        if (d < 0) {
            d += incrE;
        } else {
            d += incrNE;
            y++;
        }
        x++;
        drawPoint(x, y);
    }
    return;
}

Thus guard1 is x < x1, and guard2 is d < 0. Multiplication by two is the only multiplication. Signed decision variables are convenient because

d

and incrNE can be negative; this remains an integer arithmetic algorithm. A strictly unsigned hardware representation would need an equivalent biased or separated-sign encoding. As with the printed int skeleton, assume all intermediate values fit the chosen type; integer overflow would invalidate the mathematical decisions.

To verify the geometry, write

k = x - x_{0}

. The chosen ordinate is

y (x) = y_{0} + ⌊ \frac{2Δ y k + Δ x}{2Δ x} ⌋ .

(3)

The midpoint line decision selects exactly this nearest integer, rounding halves upward. Its increment between successive columns is zero or one. At

k = 0

and

k = Δ x

, it gives exactly

y_{0}

and

y_{1}

, respectively, so both endpoints are included and the line segment has precisely

Δ x + 1

distinct pixels.

Figure 1.
Bresenham pixels for a slope of 3/8, with the upper pixel selected at the midpoint tie
. **Details**.

For the illustrated endpoints

(1, 1)

and

(9, 4)

, the ordinates are

1, 1, 2, 2, 3, 3, 3, 4, 4

. In particular the exact ordinate at

x = 5

5/2

, and the chosen pixel is

(5, 3)

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Imperative programming / 5 / a / Solution 2026-10-31

 View more

Use a minimum stack: each linked list node caches the minimum of all values from that node down to the bottom. This handles duplicate minima without searching when one is removed.

class Stack {
  private class Node(val value: Int, val least: Int, val next: Node)
  private var top: Node = null

  def push(x: Int): Unit = {
    val m = if (top == null) x else math.min(x, top.least)
    top = new Node(x, m, top)
  }

  def pop(): Int = {
    require(!isEmpty)
    val x = top.value
    top = top.next
    x
  }

  def isEmpty: Boolean = top == null

  def min: Int = {
    require(!isEmpty)
    top.least
  }
}

The representation invariant is that the chain from top is finite and acyclic, and every reachable node q satisfies

q . l e a s t = {q . v a l u e min (q . v a l u e, q . n e x t . l e a s t) q . n e x t = n u ll, q . n e x t \neq = n u ll .

(1)

The abstraction function takes the values along this chain in top-to-bottom order. Thus pushing

x

changes

s

x : s

, and popping a nonempty

s

returns its head and leaves its tail. The cached-minimum equation follows for a new node from the previously valid chain; removing a head leaves every surviving equation unchanged. Consequently

p u s h, p o p, i s E m pt y, min each take O (1) worst-case time .

(2)

The bounds use the usual constant-cost allocation and integer arithmetic model. Storage is linear in the number of entries. min and pop require a nonempty stack; min leaves it unchanged.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2023 / Imperative programming / 1 / e / Solution 2026-10-25

 View more

Search only the suffix strictly after each candidate first index. This enforces distinct indices even when the target is twice an existing value. Compute the complement in Long to prevent integer overflow: subtracting two Int values can require 33 signed bits.

def twoSum(a: Array[Int], target: Int): (Int, Int) = {
  def lowerBound(from: Int, wanted: Long): Int = {
    var lo = from
    var hi = a.length
    while (lo < hi) {
      val mid = lo + (hi - lo) / 2
      if (a(mid).toLong < wanted) lo = mid + 1
      else hi = mid
    }
    lo
  }
  var i = 0
  while (i < a.length - 1) {
    val wanted = target.toLong - a(i).toLong
    val j = lowerBound(i + 1, wanted)
    if (j < a.length && a(j).toLong == wanted) return (i, j)
    i += 1
  }
  (0, 0)
}

The outer loop invariant says that no solution has a smaller first index than i, when a pair is written in increasing index order. A failed suffix binary search proves there is no partner for the current i, extending the excluded prefix by one. A successful return has

j > i

and

a (j) = t - a (i)

in exact integer arithmetic. At exhaustion, every possible ordered pair has been excluded, so the sentinel (0,0) means no solution. The inner loop invariant is the standard lower-bound partition, restricted to the suffix starting at i + 1.

There are at most

N - 1

suffix searches, each taking

O (lo g (N + 1))

running time, so the total is

O (N lo g (N + 1))

, customarily written

O (N lo g N)

for

N \geq 2

. Auxiliary space is

O (1)

. Empty and singleton arrays immediately return the sentinel. This is distinct-index two-sum by suffix lower bounds; a faster two-pointer technique is also possible on a sorted array, but the code here directly meets the requested search-based bound.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2023 / Imperative programming / 2 / c / Solution 2026-10-25

 View more

Under exact integer arithmetic, the intended result is $⌈ lo g_{2} x ⌉$ , using the ceiling function. A sufficient loop invariant is

i \geq 0, y = 2^{i}, i = 0 \lor 2^{i - 1} < x .

(1)

Initially

i = 0, y = 1

, and the final disjunction is true. If the guard holds, the old value

y = 2^{i}

is below

x

. Incrementing i and doubling y therefore preserves

y = 2^{i}

and makes the new lower bound

2^{i - 1} < x

true. At exit

y \geq x

. If

i = 0

, positivity of

x

forces

x = 1

; otherwise

2^{i - 1} < x \leq 2^{i}

. Both cases establish the claimed postcondition. Doubling eventually reaches or exceeds any fixed positive

x

, proving algorithm termination in this arithmetic model. This is the doubling-loop ceiling logarithm argument.

The printed Scala implementation is not correct for its entire stated Int domain. Its y is an Int. For

x > 2^{30}

, it reaches

y = 2^{30}

, wraps to

- 2^{31}

on the next doubling, then becomes zero and stays zero. The guard remains true forever. The loop invariant above is valid for the printed code only when

1 \leq x \leq 2^{30}

. Scala documents Int as a signed 32-bit value equivalent to Java's primitive int.^[ref]

A corrected implementation for every positive Int input widens the doubling variable before any multiplication:

def ceilingLog2(x: Int): Int = {
  require(x > 0)
  var i = 0
  var y = 1L
  while (y < x.toLong) {
    i += 1
    y *= 2L
  }
  i
}

Now at most 31 iterations are needed and

y \leq 2^{31}

, safely within Long. The same loop invariant proves total correctness without the overflow gap.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2023 / Imperative programming / 2 / d / Solution 2026-10-25

 View more

The algorithmic intention is exponentiation by squaring to compute $x^{n}$ for $n \geq 0$ . With exact arithmetic, its loop invariant is

i \geq 0, res u lt y^{i} = x^{n} .

(1)

Initially result = 1, y = x, and i = n. For an even integer

i = 2 q

, squaring y and replacing i by

q

preserves the product. For an odd integer

i = 2 q + 1

, first multiply result by y; then

(res u lt y) (y^{2})^{q} = res u lt y^{2 q + 1}

. The nonnegative loop variant i decreases by halving whenever positive. At exit

i = 0

, so the loop invariant yields result = x^n. There are

O (lo g (n + 1))

multiplication steps.

Two qualifications are essential for the actual source. There is no requirement that n be nonnegative: for every n <= 0 the printed function simply returns 1.0. Also, var y = x infers Int, so y *= y uses wrapping integer arithmetic, while the accumulator uses floating-point arithmetic. For example, anotherfunc(50000, 2L) returns -1794967296.0, rather than 2500000000.0. An exact-power loop invariant cannot prove a false claim about that execution.

More precisely, for positive n, after

k

iterations the remaining exponent is

⌊ n / 2^{k} ⌋

, and the Int base is the signed 32-bit representative of

x^{2^{k}}

modulo

2^{32}

. The accumulator multiplies those signed representatives for the set bits of n, in increasing bit order, with a floating-point rounding after each multiplication. This describes the actual code even when the intended power law fails. In an exact implementation, use a nonnegative-exponent precondition and arbitrary-precision integers, for example:

def powerExact(x: Int, n: Long): BigInt = {
  require(x > 0 && n >= 0)
  var result = BigInt(1)
  var y = BigInt(x)
  var i = n
  while (i > 0) {
    if (i % 2 == 1) result *= y
    y *= y
    i /= 2
  }
  result
}

The displayed loop invariant applies exactly to this version. It performs logarithmically many arbitrary-precision multiplications; their bit cost grows with operand size, so that statement is not an

O (lo g n)

bit-complexity bound. Merely making the accumulator a Double does not widen the separate Int base variable.

 Read the full article

Precondition Created 2026-10-18 Updated 2026-10-25

 View more

The condition required of a starting program state for a stated correctness guarantee. In the summation loop verification,

n \in Z

and

n \geq 0

admit

n = 0

and

n = 4

, but exclude

n = - 1

. The accompanying model assumes exact integer arithmetic and terminating elementary operations. The initial values of

i, s

need no restriction because initialization overwrites them before use.

A precondition is a logical assumption, not automatically an executable check. Writing require in a procedure states its contract; an implementation that checks or rejects invalid inputs needs that behavior specified too. Weakening a precondition admits more starts and therefore demands more proof: dropping

n \geq 0

here makes

n = - 2

a terminating counterexample to

2 s = n (n + 1)

, since initialization returns zero while

n (n + 1) = 2

 Read the full article