Write an implementation for the prime machine, Programming Languages

Assignment Help:

You should use the BToolkit to produce the answers to the questions below. Where applicable, please use the machine names and identifier names suggested in the question to help me find and mark your answers. Obviously, you can choose names for additional machines etc as required. I suggest you make a single directory for your work for this assignment (eg, ass1dir ). When you are ready to submit, go to the directory above ass1dir and create a tar file with all your work in:

tar -cvf ass1dir.tar ass1dir

then gzip it:

gzip ass1dir.tar ass1dir.tar.gz

You should generate proof conditions at each stage and examine them in the prover.

You are not required to prove all the conditions, but you should examine the ones that don't auto prove to check that they are true. Otherwise, modify your machine. All machines should have invariants which are strong enough to prove machine consistency. You should provide comments within your machines to explain what they are doing, detail any design decisions made, any problems encountered etc. If different approaches or interpretations are possible, comment your machine to explain what you have done and why. Additional comments (for example, justification for any unproved conditions for that machine) are welcome.

Question 1

Write an implementation for the Prime machine (defined 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 post condition which the initialised loop meets.

Question 2

An abstract machine, Buffer is defined at the end of this assignment sheet. Provide a refinement 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 for example, if the capacity is 8, the sequence [a, b, c, d] may correspond to:

2004_Write an implementation for the Prime machine.png

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 buff. Provide the linking invariant which captures this invariant and incorporate it in a refinement machine BufferR.

In this question, getting the linking invariant right is tricky.


Related Discussions:- Write an implementation for the prime machine

Matlab, want to do an image-mean. but image is and mean is so an error ...

want to do an image-mean. but image is and mean is so an error showing Error using ==> minus Number of array dimensions must match for binary array op. wat to do?

What is dynamic binding, Dynamic Binding: - Binding refers to the linking ...

Dynamic Binding: - Binding refers to the linking of a procedure call to the code to be executed in response to the call. Dynamic binding (late binding) means that the code associa

assembly lang. H.W, 1- Allocate array with 32bit 100 element 2- Prompt the...

1- Allocate array with 32bit 100 element 2- Prompt the user to enter the maximum or the upper bound of the random value 3- Read the value and use it generate random numbers to init

Write a program to read the file, Suppose you have a ?le orase of city and ...

Suppose you have a ?le orase of city and country names, like this: Cluj, Romania Debrecen, Hungary Klagenfurt, Austria Berlin, Germany Szeged, Hungary Budapest, Hungary Lintz, A

What is url describe their protocol, What is URL describe theri protocol? ...

What is URL describe theri protocol? URL basicallt stands for uniform resource locator. A URL is a pointer to a particular resource on the Internet at a particular location.

Visual Basic 2010 Karate Payments MDI Application, The following are requir...

The following are required for this lesson: Complete the Project "Adding New Payments," which is the Karate Payments that includes the Adding New Payments, Deleting Payments,

Java string handling, Expertsmind brings you unique solution in java assig...

Expertsmind brings you unique solution in java assignments String Handling Series signifies a sequence of character types. It has set duration of personality sequence. Onc

Program to explore page replacement algorithms, Objective: The purpose of ...

Objective: The purpose of this programming project is to explore page replacement algorithms. This can be accomplished by developing a simple simulator that implements various pag

Exploding land mines cause damage to military vehicles, In combat simulatio...

In combat simulation software, exploding land mines cause damage to military vehicles. In addition to the damage done to the vehicles themselves, we are interested in the number of

Write Your Message!

Captcha
Free Assignment Quote

Assured A++ Grade

Get guaranteed satisfaction & time on delivery in every assignment order you paid with us! We ensure premium quality solution document along with free turntin report!

All rights reserved! Copyrights ©2019-2020 ExpertsMind IT Educational Pvt Ltd