Massachusetts Institute of TechnologyDepartment of Electrical Engineering and Computer Science6.826 Principles of Computer SystemsPROBLEM SET 1Issued: Tuesday, February 5, 2002 Due: Tuesday, February 12, 2002The following problems are intended to help you understand the notions of specification and implementa-tion. Show that you can use the high-level features of Spec effectively, and don’t worry about getting everydetail of syntax exactly right. You will need to familiarize yourself with the Spec language before writingthe solutions. The best source is Handout 3 (Introduction to Spec), plus Section 9 of Handout 4 (SpecReference Manual); you should not need to read the rest of Handout 4. You will also need to understandwhat it means to implement a spec. Handout 3 explains this, and Handout 5 gives some more examples ofspecs and implementations.In each problem you are expected to write a) specification of the problem and b) implementation of thespecification. You should write both specification and implementation in the Spec language. Try to avoidusing loops or recursion to write the specs.Each specification should be a Spec function (FUNC) that accepts input and output values and returnsa Bool value. The specification should formalize the condition between the input and output values of theproblem. Make your specification as clear as possible taking advantage of the mathematical expressions andthe nondeterminism in the Spec language. Do not worry about the implementability or the efficiency in thispart of the problem, instead focus on clarity. If you need an algorithm to do one of the impleme ntations,look it up in an algorithms book.Each implementation should be a Spec atomic procedure (APROC) that accepts input values and returnsthe output values. Each implementation in this problem set should depend only on the parameters explicitlypassed as arguments to APROC and not on other parts of the program state. Make your implementationdeterministic: when called with same arguments, the procedure should return the same result. Your goal inthis part is to capture the essential idea of a deterministic implementation that could eas ily be translated toa language such as sequential Java.There are four problems in this problem set; please turn in each problem on a separate sheet of paper.Also give the amount of time you spend on each problem.Problem 1: Matrix MultiplicationA product of two matrices [aij] and [bij] is a matrix [cij] with cij=Pkaikbkj. We can represent squareinteger matrices in Spec as functions from indices to integers:TYPE Range = IN 0 .. n-1Matrix = (Range,Range) -> Inta) Write a Spec function isMatMul that accepts matrices ma, mb, mc and tests whether the matrix mc isa product of the matrices ma and mb.FUNC isMatMul(ma: Matrix, mb: Matrix, mc: Matrix) -> Bool = ...Do not use loops or recursion in this specification.b) Write a Spec atomic procedure MatMul that uses loops to compute the product of two matrices.APROC MatMul(ma: Matrix, mb: Matrix) -> Matrix = ...1Problem 2: Distribution of Prime NumbersLet x and y be positive integers.We say that y is a divisor of x if the division of x by y yields no remainder.We say that x is a prime number if x > 1 and the set of the divisors of x is {1, x}.Theorem [Chebyshev] For every integer n > 1 there exists a prime number p such that n < p < 2n.a) Write a Spec function isPrimeBetween that checks if p is a prime number between n and 2n.FUNC isPrimeBetween(p: Int, n: Int) -> Bool = ...b) Write a Spec atomic procedure primeBetween that, given n, finds a prime p such that n < p < 2n.APROC primeBetween(n: Int) -> Int = ...c) Show an example of positive integers n and p such that isPrimeBetween(p,n) is true, but yourimplementation in the b) part never returns p when called with primeBetween(n).Problem 3. Shortest PathA directed graph is a binary relation on some set. See Section 9 of Handout 4 for the definitions of somegraph operations. Let graph nodes be defined asTYPE Node = IN 1 .. na) Write a Spec function isShortestPath that tes ts whether path is the shortest path from n1 to n2 inthe graph g.FUNC isShortestPath(g: Graph[Node].G,n1: Node, n2: Node,path: SEQ Node) -> Bool = ...b) Write a Spec procedure shortestPath that given a graph g and two nodes n1 and n2 finds a shortestpath from no de n1 to node n2. Make sure that your solution implements the specification in part a),is deterministic, and has polynomial time c omplexity.APROC shortestPath(g: Graph[Node].G,n1: Node, n2: Node) -> SEQ Node = ...c) Show an example of a graph g, nodes n1 and n2 and path path such that the value of the expressionisShortestPath(g,n1,n2,path) is true, but your implementation in part b) never returns path as aresult if invoked with the procedure call
View Full Document
Unlocking...