The standard output is three lines:This is program output, excluding any interactive interpreter's display of returned values. The calls
A
2.3
Ba.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]https://www.scala-lang.org/files/archive/spec/2.11/06-expressions.html#overloading-resolution. Scala 2.11 Language Specification, §6.26.3, overload applicability and specificity
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.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.For a node tuple , write for its identifier. A predicate that is true exactly when identifiers repeat isThe 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 .
Define the directed successor relation by . Then the required predicate iswhere 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.
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. Articles by others on the same topic
There are currently no matching articles.