Read as the existence of a directed successor path from to . Then the property says every reachable ordered pair of even-valued nodes admits a connecting route through an odd-valued node. More exactly, for all even-valued with reaching , there is an odd-valued such that reaches and reaches .
The two reachability witnesses concatenate to a directed walk through . In an acyclic graph this yields an intervening node on a path. In a graph with directed cycles, the concatenation may revisit vertices. The existential witness does not say that every connecting path contains an odd-valued node, or even that an even-to-even edge is forbidden. For example edges , , , with even endpoints and odd , satisfy the property for this pair despite the direct even-to-even edge.
There are two source-notation qualifications. The displayed outer universal quantifier binds both symbols appearing as formal arguments to prop, so the whole formula is a global property of , rather than a genuinely free two-node predicate. Also the indexed ellipsis defining prop3 does not formalize path length zero. With positive-length reachability, even nodes on a cycle impose additional requirements; with reflexive reachability, choosing also imposes a requirement, and an isolated even-valued node would fail. The usual intended reading here is positive-length successor reachability. No uniqueness, acyclicity or specific path-length convention is proved by the displayed formula alone.
Define the directed successor relation by . Then the required predicate is
where denotes the natural-number information component of node . In the source's indexed notation this is .
This formulation checks both successor links against every node with the corresponding identifier, so it does not silently assume part (d)'s uniqueness condition. It checks existing successors; if every identifier must denote an actual node, add the separate referential integrity condition , or exempt an explicitly designated null identifier. The source specifies no null convention. Indeed a nonempty finite structure with two actual successors at every node cannot have strictly increasing values along all edges: following successors would eventually create a directed cycle. The implication above remains meaningful for leaves represented by absent or null successors.
For a node tuple , write for its identifier. A predicate that is true exactly when identifiers repeat is
The inequality excludes choosing the same tuple twice. The set cannot contain two copies of an identical quadruple, but it can contain distinct quadruples with equal first component and different information or successors. The negation is the usual identifier-uniqueness representation invariant, namely .
An abstract data type specifies a set of abstract values and the operations on them, including their observable behavior, independently of their concrete representation. Its operation signatures say what can be requested; its laws or preconditions and postconditions say what those requests mean.
For example a stack can be specified by an empty value, push, pop, and isEmpty, with pop(push(x,s)) returning x and leaving s. A linked list and an array can implement the same abstract data type if clients observe the same specified behavior. Encapsulation hides the representation, while a representation invariant describes which internal states are valid and an abstraction function explains which abstract value each valid internal state represents. An abstract class is a language mechanism; it is not by itself a full abstract data type specification.
The output is YY, with no newline. The variable a has static type A, although its runtime type is B. Both c.m(a) and d.m(a) therefore select the signature m(A) at compile time. The m(B) alternative is not applicable to an argument whose static type is merely A.
Both receivers refer to the same D object. Dynamic dispatch then invokes D's override of the already selected m(A) signature, printing Y twice. The static type C of c changes the visible member set, but both signatures are visible through either receiver in this example. Overload selection followed by dynamic dispatch does not select an overload from the argument's runtime type.
The standard output is three lines:
A
2.3
B
This is program output, excluding any interactive interpreter's display of returned values. The calls a.m(1) and b.m(5.6) compute squares without printing. In A, the concrete m(Int) wins over the generic method at argument 1; the string and 2.3 use m[T] and print their arguments.
For b: B[Any], the class type parameter has already become Any, so the two alternatives are m(Any) and m(Double), rather than a method with its own freely inferred type parameter. The Double alternative is more specific. It accepts 4 by numeric widening, so b.m(4) computes 16.0 without printing; b.m("B") prints B; b.m(5.6) computes a square without printing. These are applications of the Scala 2.11 method overloading rules, with the arithmetic return values discarded in statement position.[ref]
Count element reads and writes, ignoring simple-variable operations. A swap of distinct entries makes two reads and two writes, hence four expensive accesses. For , the three-reversal method therefore costs
Here if and are both even, and otherwise.
For either block-exchange version, let , , and let count element swaps. The recurrence is and, when the lengths differ,
The Euclidean algorithm preserves under this subtraction. Induction on therefore yields
Thus both block-exchange methods cost accesses, no more than the three-reversal method. Their element-access counts are identical; the iterative one avoids the recursive stack. For example a half-length rotation uses swaps instead of approximately reversal swaps.
Each single-place pass in part (iv) reads every entry once and writes every entry once, costing accesses. For , its accesses beat the block method's for and tie for . For the block method costs strictly less than . All three methods as written return without accesses for or . Repeated shifting can take quadratic time; the reversal and block methods take linear time. These comparisons concern the specified implementations, not a more general cycle-decomposition rotation using several disjoint cycles.
Exchange symmetric pairs, stopping before the middle:
PROCEDURE reverse(i, n: INTEGER);
VAR t: INTEGER;
BEGIN
  t := 0;
  WHILE t < n DIV 2 DO
    swap(i+t, i+n-1-t);
    t := t + 1
  END
END reverse;
Writing for the pre-call array, the loop invariant says that the first and last t positions of the segment already satisfy , all positions between them retain their original values, and positions outside the segment are unchanged. Each swap fixes the next symmetric pair. The loop variant decreases; the two indices are distinct and in bounds whenever the body executes. Exactly swaps reverse the segment, with the odd-length middle element left in place and no accesses for .
Assume every indicated segment lies within array bounds, and lengths are nonnegative. Use a temporary value of element type T:
PROCEDURE swap(i, j: INTEGER);
VAR x: T;
BEGIN
  x := m[i]; m[i] := m[j]; m[j] := x
END swap;

PROCEDURE blockswap(i, j, n: INTEGER);
VAR t: INTEGER;
BEGIN
  t := 0;
  WHILE t < n DO
    swap(i+t, j+t);
    t := t + 1
  END
END blockswap;
The first procedure even works for . For the second, disjointness ensures that each swap exchanges the two original entries at offset t without disturbing any other pair. Its loop invariant says that offsets below t have been exchanged, offsets from t through retain their original values, and everything outside the two segments is unchanged. The loop variant proves algorithm termination. A block exchange uses swaps and auxiliary space. The stray wp printed after this source subpart is not an additional requirement.
Accumulate the product of the matrices from left to right, which matches forward linked list traversal.
PROCEDURE cf2rat(f: fraction; VAR n, d: INTEGER);
VAR p: fraction; a, b, c, e, x: INTEGER;
BEGIN
  a := 1; b := 0; c := 0; e := 1;
  p := f;
  WHILE p # NIL DO
    x := p.head;
    a, b, c, e := a*x+b, a, c*x+e, c;
    p := p.tail
  END;
  n := a; d := c
END cf2rat;
The four-value assignment is simultaneous, as permitted by the source. With , the loop invariant after reading the prefix is
with the empty product initialized to the identity matrix. Multiplication on the right by produces exactly the four assignments above. The associativity of matrix multiplication allows this left-to-right accumulation even though the recursive conversion groups operations from the right.
At completion, the first column is the numerator/denominator pair for the whole continued fraction: the last factor sends to , and each earlier factor applies the recurrence from part (d). The vector is an algebraic device, not a finite input ratio requiring division by zero. For a nonempty list the resulting is positive; for a singleton it is . The product has determinant , so its first-column entries are coprime. Return in linear node-processing time and auxiliary space, without changing the list.
Convert the tail first and apply the reciprocal identity. Two output parameters hold the rational number's numerator and denominator.
PROCEDURE cf2rat(f: fraction; VAR n, d: INTEGER);
VAR u, v: INTEGER;
BEGIN
  IF f.tail = NIL THEN
    n := f.head; d := 1
  ELSE
    cf2rat(f.tail, u, v);
    n := f.head * u + v;
    d := u
  END
END cf2rat;
The singleton case is immediate. If the recursive call returns the tail as , then because every tail head is positive. The full value is
Structural induction on the finite nonempty linked list proves correctness, and the denominator is always positive even if the first head is negative. If the tail pair is coprime, then ; the base pair is coprime, so the result is in lowest terms. Return (head*u+v,u) after converting the tail, using linear node-processing time and linear recursive stack space.
Append each quotient directly to the output linked list, retaining a pointer to its last node. The nodes are required output; auxiliary variables remain simple integers and pointers.
PROCEDURE rat2cf(n, d: INTEGER): fraction;
VAR first, last, p: fraction; q, r: INTEGER;
BEGIN
  first := NIL; last := NIL;
  REPEAT
    q := n DIV d; r := n MOD d;
    NEW(p); p.head := q; p.tail := NIL;
    IF first = NIL THEN first := p
    ELSE last.tail := p
    END;
    last := p;
    n := d; d := r
  UNTIL d = 0;
  RETURN first
END rat2cf;
At the start of each iteration, d is positive, and the output prefix consists exactly of the quotients already obtained by the Euclidean algorithm. last points to its final node, or both first and last are null when the prefix is empty. The current ratio n/d is the unexpanded tail of the original continued fraction. The quotient/remainder step extends that prefix by the same value as the recursive version, then replaces the unexpanded ratio by its reciprocal residual tail. If the remainder is zero, no tail remains and the loop stops before another division.
The loop variant is the positive current denominator, which strictly decreases after each nonfinal iteration. The input denominator is positive, so at least one node is allocated, including for zero or an integral ratio. This is the same exact conversion with auxiliary space, excluding the returned list, and no input mutation.
Use the Euclidean algorithm with floor quotient and nonnegative remainder, including for a negative numerator:
PROCEDURE rat2cf(n, d: INTEGER): fraction;
VAR q, r: INTEGER; p: fraction;
BEGIN
  q := n DIV d; r := n MOD d;
  NEW(p); p.head := q; p.tail := NIL;
  IF r # 0 THEN p.tail := rat2cf(d, r) END;
  RETURN p
END rat2cf;
For , Euclidean division gives with . If , the singleton [q] is exact. Otherwise
so the recursive tail represents . Its numerator is positive and greater than its denominator, so every tail head is a positive integer. The new denominator is strictly smaller than , proving algorithm termination by descent through the positive integers.
The returned list represents exactly . For example gives [-3,1,2]; truncating negative division toward zero would violate the required positivity of the tail. There are Euclidean algorithm steps, with output allocation and recursive stack depth linear in the number of generated nodes.
Print a prefix while following the linked list, counting how many closing parentheses remain. The final reciprocal can be printed without parentheses.
PROCEDURE printCF(f: fraction);
VAR p: fraction; opened: INTEGER;
BEGIN
  p := f; opened := 0;
  Out.Int(p.head, 0);
  p := p.tail;
  WHILE p # NIL DO
    IF p.tail = NIL THEN
      Out.String("+1/"); Out.Int(p.head, 0)
    ELSE
      Out.String("+1/("); Out.Int(p.head, 0);
      opened := opened + 1
    END;
    p := p.tail
  END;
  WHILE opened > 0 DO
    Out.String(")"); opened := opened - 1
  END
END printCF;
The first loop invariant says that p is the next unprinted linked list node, the printed text is the correct expression prefix, and opened counts its unmatched opening parentheses. The final node contributes no opening parenthesis; the second loop invariant says that precisely opened closing parentheses remain. Thus [1,2,3,4,5] produces 1+1/(2+1/(3+1/(4+1/5))). A singleton prints just its head. If the first head is negative, its leading minus remains a valid prefix; subsequent heads are positive.
The precondition is a finite nonempty continued fraction list. Every dereference is made only for a nonnull pointer. The procedure uses auxiliary space and time linear in the number of nodes, apart from printing their digits. The source's claimed strict upper bound has an exception under its stated definition: [x0,1] represents . None of these algorithms relies on that incorrect strict bound.
The second procedure should reach large outputs faster, because the first makes exactly expensive MOD operations when processing argument , whereas the second tries only up to the square root of a shrinking residual, with at most successful DIV operations. Each successful division also requires a successful MOD test; each outer iteration adds one final unsuccessful MOD test. Thus its expensive-operation count is per argument, and at most cumulatively through argument , compared with for direct counting.
The speedup is not an assertion that every single call uses fewer divisions: for , the second code makes three MOD tests and two DIV operations, while the first makes four MOD tests. Small constant costs can go either way. The many small prime factors in highly composite numbers also shrink the residual early, which often helps further; the cumulative comparison includes every preceding argument, not only the printed records.
Use trial division on a shrinking residual. Once the trial divisor exceeds its square root, any residual larger than one is itself prime.
PROCEDURE divisors(n: INTEGER): INTEGER;
VAR residual, trial, exponent, answer: INTEGER;
BEGIN
  residual := n; trial := 2; answer := 1;
  WHILE trial * trial <= residual DO
    exponent := 0;
    WHILE residual MOD trial = 0 DO
      residual := residual DIV trial;
      exponent := exponent + 1
    END;
    answer := answer * (exponent + 1);
    trial := trial + 1
  END;
  IF residual > 1 THEN answer := 2 * answer END;
  RETURN answer
END divisors;
For the outer loop invariant, let be the set of primes below trial and their exponents in the original . Then
and residual has no prime factor below trial. If trial divides the residual it must therefore be prime: a composite trial value would have a smaller prime factor, contradicting this clause. If it does not divide, the zero exponent contributes the factor .
For the inner loop invariant, let be the residual on entry. Then . Each exact division reduces the positive residual by at least a factor of two, so this loop terminates. At exit the exponent is the full multiplicity of trial; multiplying by exponent+1 preserves the outer loop invariant. The outer loop terminates because trial increases and residual never increases. When it exits, a composite residual would have a prime factor at most its square root, yet every smaller trial factor has already been excluded. Hence the residual is or a single remaining prime of exponent .
The procedure computes in unit-cost time and auxiliary space, with the separate successful divisions bounded by . No array or table of primes is needed, and correctly returns .

Pinned article: Introduction to the OurBigBook Project

Welcome to the OurBigBook Project! Our goal is to create the perfect publishing platform for STEM subjects, and get university-level students to write the best free STEM tutorials ever.
Everyone is welcome to create an account and play with the site: ourbigbook.com/go/register. We belive that students themselves can write amazing tutorials, but teachers are welcome too. You can write about anything you want, it doesn't have to be STEM or even educational. Silly test content is very welcome and you won't be penalized in any way. Just keep it legal!
We have two killer features:
  1. topics: topics group articles by different users with the same title, e.g. here is the topic for the "Fundamental Theorem of Calculus" ourbigbook.com/go/topic/fundamental-theorem-of-calculus
    Articles of different users are sorted by upvote within each article page. This feature is a bit like:
    • a Wikipedia where each user can have their own version of each article
    • a Q&A website like Stack Overflow, where multiple people can give their views on a given topic, and the best ones are sorted by upvote. Except you don't need to wait for someone to ask first, and any topic goes, no matter how narrow or broad
    This feature makes it possible for readers to find better explanations of any topic created by other writers. And it allows writers to create an explanation in a place that readers might actually find it.
    Figure 1.
    Screenshot of the "Derivative" topic page
    . View it live at: ourbigbook.com/go/topic/derivative
  2. local editing: you can store all your personal knowledge base content locally in a plaintext markup format that can be edited locally and published either:
    This way you can be sure that even if OurBigBook.com were to go down one day (which we have no plans to do as it is quite cheap to host!), your content will still be perfectly readable as a static site.
    Figure 5. . You can also edit articles on the Web editor without installing anything locally.
    Video 3.
    Edit locally and publish demo
    . Source. This shows editing OurBigBook Markup and publishing it using the Visual Studio Code extension.
  3. https://raw.githubusercontent.com/ourbigbook/ourbigbook-media/master/feature/x/hilbert-space-arrow.png
  4. Infinitely deep tables of contents:
    Figure 6.
    Dynamic article tree with infinitely deep table of contents
    .
    Descendant pages can also show up as toplevel e.g.: ourbigbook.com/cirosantilli/chordate-subclade
All our software is open source and hosted at: github.com/ourbigbook/ourbigbook
Further documentation can be found at: docs.ourbigbook.com
Feel free to reach our to us for any help or suggestions: docs.ourbigbook.com/#contact