Hi,
Attached are two programs that represent one-way and two-way traffic on
a road. I can get the programs to produce reasonable results that match
our intuitive ideas of roads.
However, I have 2 question about the programs:
1)I cannot get the result suggested by the author that t1 should give
true in prog1 and false in prog2.
2)My second question is more theoretical. It is stated by the author
that type checking and excitability provide verification. In this case
verification probably means checking that an instance is consistent with
its type class. Does verification using these techniques in Haskell have
any firmer logical foundation than say doing the verification in Java? I
am aware that Haskell uses inference for type checking, but is the net
result superior to compilers that do not use inference? Also, is Haskell
execution based purely on logic?
Regards,
Pat
This message has been scanned for content and viruses by the DIT Information
Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie
-- Ontologies of One-way Roads by Sumit Sen
-- http://ifgi.uni-muenster.de/~sumitsen/sen_Font05.pdf
-- Two way roads
class Link link object | link -> object where
from, to::link -> object
other::Eq object => link -> object -> object
other link object | object == from link = to link
| object == to link = from link
| otherwise = error "not linked"
class Path path object where
move :: path -> object -> object
class Named object name | object -> name where
name :: object -> name
class LocatedAt object link where
location :: object -> link
--Node
type Name = String
data Node = Node Name deriving (Eq, Show)
-- Edge: "A sequence of line segments with nodes at each end"
data Edge = Edge Node Node deriving Show
-- Car
data Car = Car Node deriving (Eq, Show)
type Cars = [Car]
-- a Node is a named object
instance Named Node Name where
name (Node n) = n
-- an Edge as Link between Nodes
instance Link Edge Node where
from (Edge node1 node2) = node1
to (Edge node1 node2) = node2
-- a Car located at a Node
instance LocatedAt Car Node where
location (Car node) = node
-- Road Element
data RoadElement = RoadElement Edge deriving Show
class (Path path conveyance ) => Conveyance conveyance path object where
transport :: path -> conveyance -> object -> object
-- RoadElements as Links between Nodes
instance Link RoadElement Node where
from (RoadElement edge) = from edge
to (RoadElement edge) = to edge
-- RoadElements as Paths for Cars
instance Path RoadElement Car where
move (RoadElement edge) (Car node) = Car (other edge node)
-- Algebraic specifications usually depend on (automatic) theorem provers for
verification of specifications.
-- For our case however type checking and executablity form the basis of
verification of our specifications in Haskell.
-- This is done by executing test scripts such as
-- As orignal paper
start = Node "start"
end = Node "end"
theEdge = Edge start end
theCar = Car start
theRoadElement = RoadElement theEdge
t1 = location (move theRoadElement theCar) == end
-- Some additional tests
-- If start end switched then no linked error
theEdge2 = Edge start end
theEdge3 = Edge end start
theCar2 = Car start
theCar3 = Car end
theRoadElement2 = RoadElement theEdge2
theRoadElement3 = RoadElement theEdge3
t2 = location (move theRoadElement2 theCar2) == end
t3 = location (move theRoadElement3 theCar3) == start
-- In prog2
-- other (Edge (Node "start") (Node "end")) (Node "end")
-- gives start
-- other (Edge (Node "start") (Node "end")) (Node "start")
-- gives end
-- Which is what we would expect for a two way street.
-- I can get t1, t2 and t3 to give expected results, but I *cannot* get the
following to work
-- Thus t1 will be true if spec 1 is used and false if spec2 is used deciding
if the road specification is of a one way road.
-- Ontologies of One-way Roads by Sumit Sen
-- http://ifgi.uni-muenster.de/~sumitsen/sen_Font05.pdf
--One-way road
class Link link object | link -> object where
from, to::link -> object
other::Eq object => link -> object -> object
other link object | object == from link = to link
| otherwise = error "not linked"
class Path path object where
move :: path -> object -> object
class Named object name | object -> name where
name :: object -> name
class LocatedAt object link where
location :: object -> link
--Node
type Name = String
data Node = Node Name deriving (Eq, Show)
-- Edge: "A sequence of line segments with nodes at each end"
data Edge = Edge Node Node deriving Show
-- Car
data Car = Car Node deriving (Eq, Show)
type Cars = [Car]
-- a Node is a named object
instance Named Node Name where
name (Node n) = n
-- an Edge as Link between Nodes
instance Link Edge Node where
from (Edge node1 node2) = node1
to (Edge node1 node2) = node2
-- a Car located at a Node
instance LocatedAt Car Node where
location (Car node) = node
-- Road Element
data RoadElement = RoadElement Edge deriving Show
class (Path path conveyance ) => Conveyance conveyance path object where
transport :: path -> conveyance -> object -> object
-- RoadElements as Links between Nodes
instance Link RoadElement Node where
from (RoadElement edge) = from edge
to (RoadElement edge) = to edge
-- RoadElements as Paths for Cars
instance Path RoadElement Car where
-- move (RoadElement edge) (Car node) = Car (other edge node)
move (RoadElement edge) (Car node) = Car (other edge node)
-- Algebraic specifications usually depend on (automatic) theorem provers for
verification of specifications.
-- For our case however type checking and executablity form the basis of
verification of our specifications in Haskell.
-- This is done by executing test scripts such as
start = Node "start"
end = Node "end"
theEdge = Edge start end
theCar = Car start
theRoadElement = RoadElement theEdge
t1 = location (move theRoadElement theCar) == end
-- In prog1
-- other (Edge (Node "start") (Node "end")) (Node "start")
-- gives end
-- In prog1
-- other (Edge (Node "start") (Node "end")) (Node "end")
-- Gives Exception: not linked
-- But I *cannot* get the following to work
-- Thus t1 will be true if spec 1 is used and false if spec2 is used deciding
if the road specification is of a one way road._______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
