/* Labeled Digraph ADT Interface, Immutable Method-Chaining Functions CSci 555: Functional Programming, Spring 2019 H. Conrad Cunningham, Professor Computer and Information Science University of Mississippi 1234567890123456789012345678901234567890123456789012345678901234567890 2016-03-23: Developed Scala version from 2015 Haskell version 2016-03-21: Made comments more consistent with 2018 ELIFP Ch. 23 ## Specification of Labeled Digraph ADT ### Notation We use the following notation and terminology to describe the abstract data type's model and its semantics. - (ForAll x, y :: p(x,y)) is true if and only if predicate p(x,y) is true for all values of x and y. - (Exists x, y :: p(x,y)) is true if and only if there is at least one pair of values x and y for which p(x,y) is true. - (# x, y :: p(x,y)) yields a count of pairs (x,y) for which p(x,y) is true. - <=> denotes logical equivalence. p <=> q is true if and only if the logical (Boolean) values p and q are equal (i.e. both true or both false). - x IN C is true if and only if value x is member of a collection C (such as a set, bag, or sequence). Similarly, x NOT_IN C denotes the negation of x IN C. - A type consists of a set of values and a set of operations. We sometimes say a value is IN a type to mean the value is IN the set associated with the type. - For sets C and D, C UNION D denotes set union, that is, a set that includes all the element of both C and D. - For sets C and D, C INTERSECT D denotes set intersection, that is, a set that includes all elements that are both in C and in D. - For sets C and D, C - D denotes set difference, that is, the set C with all elements of set D removed. - For sets C and D, C SUBSET_OF D denotes that C is subset of D, that is, all the elements of C also occur in D. - A Cartesian product of two sets C and D is the set of all ordered pairs (x,y) where x IN C and y IN D. - A tuple such as (x,*) appearing in a collection such as { (x,*) } denotes element x grouped with all possible values of the second component. Note: We could also write { (x,*) } using a quantification as: { (x,c) :: c IN some_domain } - A relation on sets C and D is a subset of the Cartesian product of C and D. That is, a set of tuples. - A function on sets C and D is a special case of a relation on C and D where each value from C occurs in at most one tuple in the relation. - A total function is defined for all elements of its domain. A partial function is defined for a subset of the elements of its domain. ### Sets The abstract data type being defined is named Digraph. We specify that this abstract data type be represented by a Scala trait Digraph[VertexType, VertexLabelType, EdgeLabelType], which has three type parameters (i.e. sets): 1. Type (or set) VertexType denotes the possible vertices (i.e. vertex identifiers) in the Digraph. 2. Type (or set) VertexLabelType denotes the possible labels on vertices in the Digraph. 3. Type (or set) EdgeLabelType denotes the possible labels on edges in the Digraph. Given this ADT defines a digraph, edges can be identified by ordered pairs (tuples) of vertices. Values of the above types, in particular the labels, may have several components. ### Semantics We model the state of the instance of the Labelled Digraph ADT with an abstract value G such that G = (V,E,VL,EL) with G's components satisfying the following Labelled Digraph Properties. - V is a finite subset of values from the set VertexType. V denotes the vertices (or nodes) of the digraph. - Any two elements of V can be compared for equality. - E is a binary relation on the set V. A pair (v1,v2) IN E denotes that there is a directed edge from v1 to v2 in the digraph. Note that this model allows at most one (directed) edge from a vertex v1 to vertex v2. It allows a directed edge from a vertex to itself. Also, because vertices can be compared for equality, any two edges can also be compared for equality. - VL is a total function from set V to the set VertexLabelType. - EL is a total function from set E to the set EdgeLabelType. #### Interface invariant We define the following interface invariant for the Labelled Digraph ADT: Any valid labelled digraph instance G, appearing in either the arguments or return value of a public ADT operation, must satisfy the Labelled Digraph Properties. #### Constructive semantics We specify the various ADT operations below using their type signatures, preconditions, and postconditions. Along with the interface invariant, these comprise the (implementation-independent) specification of the ADT (i.e. its abstract interface). In these assertions, for a digraph object g that satisfies the invariants: - G(g) denotes the graph object g's abstract model (V,E,VL,EL) as described above. - G(this) represents the receiver graph object's state before the operation. - G(this') represents the receiver graph object's state after the operation. - Result denotes the return value of function. Given this family of implementations uses immutable graph objects, every operation, both accessor and mutator, has a postcondition conjunct: G(this) = G(this') Note: For an implementation allowing mutable graph objects, this requirement may be relaxed for some mutators. However, it should still hold for all accessors. */ trait Digraph[A,B,C] { // A = VertexType, B = VertexLabelType, // C = EdgeLabelType /* A zero-parameter constructor has the following preconditions and postconditions. Pre: True Post: G(this') = ({},{},{},{}) */ /* Accessor isEmpty returns true if and only if this graph is empty. Pre: G(this) =(V,E,VL,EL) Post: Result = (V == {} && E == {}) */ def isEmpty: Boolean /* Mutator addVertex(nv,nl) inserts vertex nv with label nl into this graph and returns the resulting graph. Pre: G(this) = (V,E,VL,EL) && nv NOT_IN V Post: G(Result) = (V UNION {nv}, E, VL UNION {(nv,nl)}, EL) */ def addVertex(nv: A, nl: B): Digraph[A,B,C] /* Mutator removeVertex(ov) deletes vertex ov from this graph and returns the resulting graph. Pre: G(this) = (V,E,VL,EL) && ov IN V Post: G(Result) = (V', E', VL', EL') where V' = V - {ov} E' = E - {(ov,*),(*,ov)} VL' = VL - {(ov,*)} EL' = EL - {((ov,*),*),((*,ov),*)} */ def removeVertex(ov: A): Digraph[A,B,C] /* Mutator updateVertex(ov,nl) changes the label on vertex ov in this graph to be nl and returns the resulting graph. Pre: G(this) = (V,E,VL,EL) && ov IN V Post: G(Result) = (V - {ov}, E, VL', EL) && G(this) = G(this') where VL' = (VL - {(ov,VL(ov))}) UNION {(ov,nl)} */ def updateVertex(ov: A, nl: B): Digraph[A,B,C] /* Accessor getVertexLabel(ov) returns the label from vertex ov in this graph. Pre: G(this) = (V,E,VL,EL) && ov IN V && G(this) = G(this') Post: Result = VL(ov) */ def getVertexLabel(ov: A): B /* Accessor hasVertex(v) returns true if and only if ov is a vertex of this graph. Pre: G(this) = (V,E,VL,EL) && ov IN VertexLabelType Post: G(Result) = ov IN V */ def hasVertex(v: A): Boolean /* Mutator addEdge(v1,v2,nl) inserts an edge from vertex v1 to vertex v2 in this graph and returns the resulting graph. Pre: G(this) = (V,E,VL,EL) && v1 IN V && v2 IN V && (v1,v2) NOT_IN E Post: G(Result) = (V, E', VL, EL') && G(this) = G(this') where E' = E UNION {(v1,v2)} EL' = EL UNION {((v1,v2),nl)} */ def addEdge(v1: A, v2: A, nl: C): Digraph[A,B,C] /* Mutator removeEdge(v1,v2) deletes the edge from vertex v1 to vertex v2 from this graph and returns the resulting graph. Pre: G(this) = (V,E,VL,EL) V - {ov} && (v1,v2) IN E Post: G(Result) = (V, E - {(v1,v2)}, VL, EL - { ((v1,v2),*) } */ def removeEdge(v1: A, v2: A): Digraph[A,B,C] /* Mutator updateEdge(v1,v2,nl) changes the label on the edge from vertex v1 to vertex v2 in this graph to have label nl and returns the resulting graph. Pre: G(this) = (V,E,VL,EL) && (v1,v2) IN E Post: G(Result) = (V, E, VL, EL') && G(this) = G(this') where EL' = (EL - {((v1,v2),*)}) UNION {((v2,v2),nl) */ def updateEdge(v1: A, v2: A, nl: C): Digraph[A,B,C] /* Accessor getEdgeLabel(v1,v2) returns the label on the edge from vertex v1 to vertex v2 in this graph. Pre: G(this) = (V,E,VL,EL) && (v1,v2) IN E Post: Result = EL((v1,v2)) */ def getEdgeLabel(v1: A, v2: A): C /* Accessor hasEdge(v1,v2) returns true if and only if there is an edge from a vertex v1 to a vertex v2 in this graph. Pre: G(this) = (V,E,VL,EL) Post: Result = (v1,v2) IN E */ def hasEdge(v1: A, v2: A): Boolean /* Accessor allVertices returns a sequence of all the vertices in this graph. The sequence is represented by a builtin Scala list. Pre: G(this) = (V,E,VL,EL) Post: (ForAll ov: ov IN Result <=> ov IN V) && length(Result) = size(V) */ def allVertices: List[A] /* Accessor fromEdges(v1) returns a sequence of all vertices v2 such that there is an edge from vertex v1 to vertex v2 in this graph. The sequence is represented by a builtin Scala list. Pre: G(this) = (V,E,VL,EL) && v1 IN V Post: (ForAll v2: v2 IN Result <=> (v1,v2) IN E) && length(Result) = (# v2 :: (v1,v2) IN E) Note: Function fromEdges(v1) should return an empty list when v1 does not appear in this graph, so that it can work well with the Wizard's Adventure game. We should redefine the precondition and postcondition to specify this behavior. */ def fromEdges(v1: A): List[A] /* Accessor allVerticesLabels returns a sequence of all pairs (v,l) such that v is a vertex and l is it's label in this graph. The sequence is represented by a builtin Scala list. Pre: G(this) = (V,E,VL,EL) Post: (ForAll v, l: (v,l) IN Result <=> (v,l) IN VL) && length(Result) = size(VL) */ def allVerticesLabels: List[(A,B)] /* Accessor fromEdgesLabels(v1) returns a sequence of all pairs (v2,l) such that there is an edge (v1,v2) labeled with l in this graph. Pre: G(this) = (V,E,VL,EL) && v1 IN V Post: (ForAll v2, l :: (v2,l) IN Result <=> ((v1,v2),l) IN EL) && length(Result) = (# v2 :: (v1,v2 ) IN E) Note: Function fromEdgesLabels(v1) should return an empty list when v1 does not appear in this graph, so that it can work well with the Wizard's Adventure game. We should redefine the precondition and postcondition to specify this behavior. */ def fromEdgesLabels(v1: A): List[(A,C)] /* A class that extends this trait will likely need to override toString and/or equals to give them appropriate definitions. */ }