Consider a system that handles railway connections as it associates (source) cities to all their corresponding destinations. The requirements of the system are as follows: 1. A source city may have connections to possibly multiple destination cities. 2. Multiple source cities may share the same group of destination cities. We introduce type CITY . A possible state of the system is shown below as it is captured by variable connections: connections = { Montreal → {Ottawa, Kingston, Quebec, Halifax}, Ottawa → {Montreal, Toronto}, Toronto → {Montreal, Ottawa}, Halifax → {Montreal, Quebec}, Quebec → {Montreal, Halifax}, Kingston → {Montreal} } 1. Is connections a binary relation? Explain why, and if so express this formally. 2. In the expression connections ∈ (...), what would the RHS be? 3. Is connections a function? If so, define the function formally, and reason about the properties of injectivity, surjectivity and bijectivity. 4. Describe the meaning and evaluate the following expression: {Montreal, Halifax} ◁ connections 5. Describe the meaning and evaluate the following expression: connections ▷ {{Montreal, Halifax}} 6. Describe the meaning and evaluate the following expression: {Montreal, Quebec, Halifax} −◁ connection 7. Describe the meaning and evaluate the following expression: connections −▷ {{Ottawa, Kingston, Quebec, Halifax}, {Montreal, Ottawa}, {Montreal}} (I mean 'domain subtraction' by this −◁ and 'range subtraction' by this −▷, don't know how to include the symbols) 8. Describe the meaning and evaluate the following expression that forms a post-condition to some operation: connections′ = connections⊕{ Halifax → {Montreal, Charlottetown, Quebec}, Charlottetown → {Halifax} } 9. Assume that we need to add a new entry into the database table represented by connections. We have decided NOT to deploy a precondition. What could be the consequences to the system if we deployed a) set union and b) relational overriding? 10. Consider operation AddConnection to add a new entry to the table, defined by the following pair of assertions: city? ̸∈ dom connections connections′ = connections ∪ {city? → destinations?} What would be result of the call AddConnection(Montreal, (Boston, NYC)), and in the case of failure, whom should we blame and why? (I mean "not a member" by this ̸∈) 11. Consider the following modification to the postcondition of AddConnection: connections′ = connections ⊕ {city? → destinations?} What would be result of the call AddConnection(Kingston, (Boston, NYC))? In the absence of a precondition, can relational overriding unconditionally capture the intent of the operation? 12. Consider the following state schema in the Z specification language: _RailwayManagement____________________________________________________________ |cities : PCITY |connections : CITY ↛ PCITY |______________ |cities = dom connections ____________________________________________________________________________ Define the schema for operation GetDestinations which returns all destinations for a given city. (I mean "partial function" by this ↛ ) 13. (PROGRAMMING) Define global variable connections in Common LISP and populate it with some sample data. Demonstrate that the variable indeed contains the ordered pairs as shown above. 14. Describe how you would validate variable connections, i.e. how to show that it holds a function. 15. (PROGRAMMING) Define a predicate function, isfunctionp, in Common LISP that reads a variable like connections and indicates if the variable corresponds to a function or not. 16. (PROGRAMMING) Define function GetDestinations in Common LISP.
Consider a system that handles railway connections as it associates (source) cities to all their corresponding destinations. The requirements of the system are as follows:
1. A source city may have connections to possibly multiple destination cities.
2. Multiple source cities may share the same group of destination cities.
We introduce type CITY . A possible state of the system is shown below as it is captured by variable connections:
connections =
{
Montreal → {Ottawa, Kingston, Quebec, Halifax},
Ottawa → {Montreal, Toronto},
Toronto → {Montreal, Ottawa},
Halifax → {Montreal, Quebec},
Quebec → {Montreal, Halifax},
Kingston → {Montreal}
}
1. Is connections a binary relation? Explain why, and if so express this formally.
2. In the expression connections ∈ (...), what would the RHS be?
3. Is connections a function? If so, define the function formally, and reason about the properties of injectivity, surjectivity and bijectivity.
4. Describe the meaning and evaluate the following expression:
{Montreal, Halifax} ◁ connections
5. Describe the meaning and evaluate the following expression:
connections ▷ {{Montreal, Halifax}}
6. Describe the meaning and evaluate the following expression:
{Montreal, Quebec, Halifax} −◁ connection
7. Describe the meaning and evaluate the following expression:
connections −▷ {{Ottawa, Kingston, Quebec, Halifax}, {Montreal, Ottawa}, {Montreal}}
(I mean 'domain subtraction' by this −◁ and 'range subtraction' by this −▷, don't know how to include the symbols)
8. Describe the meaning and evaluate the following expression that forms a post-condition to some operation:
connections′ = connections⊕{
Halifax → {Montreal, Charlottetown, Quebec},
Charlottetown → {Halifax}
}
9. Assume that we need to add a new entry into the
10. Consider operation AddConnection to add a new entry to the table, defined by the following pair of assertions:
city? ̸∈ dom connections
connections′ = connections ∪ {city? → destinations?}
What would be result of the call AddConnection(Montreal, (Boston, NYC)), and in the case of failure, whom should we blame and why?
(I mean "not a member" by this ̸∈)
11. Consider the following modification to the postcondition of AddConnection:
connections′ = connections ⊕ {city? → destinations?}
What would be result of the call AddConnection(Kingston, (Boston, NYC))? In the absence of a precondition, can relational overriding unconditionally capture the intent of the operation?
12. Consider the following state schema in the Z specification language:
_RailwayManagement____________________________________________________________
|cities : PCITY
|connections : CITY ↛ PCITY
|______________
|cities = dom connections
____________________________________________________________________________
Define the schema for operation GetDestinations which returns all destinations for a given city.
(I mean "partial function" by this ↛ )
13. (PROGRAMMING) Define global variable connections in Common LISP and populate it with some sample data. Demonstrate that the variable indeed contains the ordered pairs as shown above.
14. Describe how you would validate variable connections, i.e. how to show that it holds a function.
15. (PROGRAMMING) Define a predicate function, isfunctionp, in Common LISP that reads a variable like connections and indicates if the variable corresponds to a function or not.
16. (PROGRAMMING) Define function GetDestinations in Common LISP.
Step by step
Solved in 3 steps
