Write an implementation for the Prime machine (de?ned at the end of the assignment sheet). Provide a suitable invariant and variant for any loop you use. Provide comments in your machine stating the precondition and postcondition which the initialised loop meets.

An abstract machine, Bu?er is de?ned at the end of this assignment sheet. Provide a re?nement of this machine which stores the queue in an array:

aa : 1 . . qlen → ELEM

When elements are removed from the front of the queue, the array itself is not altered but the positions become available for overwriting. When adding elements, once the end of aa is reached, wrap-around can occur if positions at the front of aa are available. Thus forexample, if the capacity is 8, the sequence [a, b, c, d] may correspond to:

etc (where * indicates any element).

To do this you will need to introduce some further state variables to keep track of the situation in the array and to enable you to relate the state of aa to the state of bu? . Provide the linking invariant which captures this invariant and incorporate it in a re?nement machine BufferR.

Posted Date: 3/8/2013 1:25:36 AM | Location : United States

Ask an Expert

Related Discussions:- Implementation for the prime machine, Assignment Help, Ask Question on Implementation for the prime machine, Get Answer, Expert's Help, Implementation for the prime machine Discussions

Write discussion on Implementation for the prime machine
Your posts are moderated

Write your message here..

Related Questions

What is cts and cls, What is CTS and CLS? CLS stands for common langua... What is CTS and CLS? CLS stands for common language specification CTS stands for common type system.

What information is stored in a typical TLB table entry, In a simple paging... In a simple paging system, what information is stored in a typical Look-aside Buffers  TLB table entry? A classical TLB table entry contains page# and frame#, while a logical

What are the blocks of microprocessor based system, What are the blocks of ... What are the blocks of microprocessor based system 1.  The Memory and I/O System 2.  The DOS Operating System 3.  The Microprocessor

Show the characteristic of cache memory, Q. Show the characteristic of cach... Q. Show the characteristic of cache memory? The essential characteristic of cache memory is its fast access time. So very little or no time should be wasted when searching for

What is meant by refreshing of the screen, What is meant by refreshing of t... What is meant by refreshing of the screen?  Some method is required for maintaining the picture on the screen. Refreshing of screen is completed by keeping the phosphorus glowi

Explain the commonly used code optimization techniques, Explain briefly any... Explain briefly any three of the commonly used code optimization techniques. 1. Common sub expression elimination: In given expression as "(a+b)-(a+b)/4", in such "common

Differentiate among validation and exception testing, Differentiate between... Differentiate between validation and exception testing. - Validation testing is done to test software in conformance to requirements specified. It aims to demonstrate that soft

Equivalences & rewrite rules - artificial intelligence, Equivalences & Rewr... Equivalences & Rewrite Rules - artificial intelligence: Along with allowing us to verify trivial theorems, tautologies make us able to establish that definite sentences are say

Explain implementation of circuits from boolean expression, Explain Impleme... Explain Implementation of the Circuits From the Boolean Expression? If the operation of the circuit is defined by a Boolean expression, a logic-circuit diagram can he implement

Simplify pos expression, Q. For function F(X, Y, Z) = ∑(1, 2, 3, 5, 6) usin... Q. For function F(X, Y, Z) = ∑(1, 2, 3, 5, 6) using TRUTH TABLE only 1.  Find POS expression 2.  Simplify POS expression 3.  Implement this simplified expression using t