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:

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.

Posted Date: 3/9/2013 5:18:00 AM | Location : United States

Ask an Expert

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

Write discussion on Write an implementation for the prime machine
Your posts are moderated

Write your message here..

Related Questions

Sizes of the clusters influence-k-means program, Objective: to show if th... Objective: to show if the sizes of the clusters influence the communication cost among a set on nodes Write a K-Means  program  for a set of M points randomly distributed on an

Calculate the total price to purchase all the components req, Calculate the... Calculate the total price to purchase all the components required to build a state-of-the-art gaming computer from components available on the internet. Before attempting this exer

Define the syntax of for loop, Define the Syntax of FOR Loop? The unive... Define the Syntax of FOR Loop? The universal form of this statement is for(initialization;condition;increment/decrement)             { statements;             }

C.., I am still waiting on a quote from you I am still waiting on a quote from you

Java source code classes and objects, Design and implement a stringed music... Design and implement a stringed musical instrument class using the following guidelines: a. Data fields for your instrument should include number of strings, an array of stri

Programs for shell scripts, 1. Write a bash shell script which searches thr... 1. Write a bash shell script which searches through your folders for files with the extension *.tex, and then interactively deletes the corresponding *.aux, *.dvi and *.log files (

Python , Write a script that will list and count all of the images in a giv... Write a script that will list and count all of the images in a given HTML web page. Each image starts with

Computer design project , I''m studying electrical engineering, and this se... I''m studying electrical engineering, and this semester im taking course that called Computer Design. in this course they need me to a final project about any thing we took during

Fortran function for find and print out all prime number, Write a Fortran L... Write a Fortran LOGICAL FUNCTION, called "is_prime", which determines if a given integer value is a prime number or not (A prime number is a natural number which has only two disti

Systems of differential equations, In this section we need to take a brief ... In this section we need to take a brief look at systems of differential equations which are larger than 2 x 2. The problem now is not like the first few sections where we looked at