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

Computes the least squares fit of the data, Your solution to the problem sh...

Your solution to the problem should be housed within a while loop, which allows the grader to test your solution repeatedly without having to re-execute the script, as shown in cla

Write a program to show twenty ellipses, Write a Program to Show Twenty Ell...

Write a Program to Show Twenty Ellipses 1. Write a program to show twenty ellipses which move away from the mouse pointer. Their initial locations should be random.

Introduction to javascript, This is the programming language of the Web. It...

This is the programming language of the Web. It is mainly used for validating forms. JavaScript & Java can be associated to each other. There exist several other differences betwee

Data modelling-use case diagram and sequence diagram, On-line fair and ethi...

On-line fair and ethical share trading system (Olfest) A system is required that allows on-line customers to buy and sell stock market shares in a selection of companies. B

Learning when and how to use a while loop, 1.  A function that produces the...

1.  A function that produces the Collatz sequence and counts the number of terms. 2.  A main function that calculates interesting values about the Collatz sequence. 1.The Col

3-Tier Architecture in asp.net, I am getting error at business layer object...

I am getting error at business layer object in code behind page.

Prolog predicate to remove nth element, Write a Prolog predicate remove_nth...

Write a Prolog predicate remove_nth(N,L1,L2) that is true if list L2 is just list L1 with its Nth element removed. If L1 does not have an Nth element then the predicate should fail

Program for tube challenge route, 1. Introduction The Tube Challenge is ...

1. Introduction The Tube Challenge is a Guinness World Records challenge that tests both the physical and mental abilities of the person trying to break it. The main components

Discuss the php operators, Question 1 Explain the history of Internet ...

Question 1 Explain the history of Internet Question 2 What are the advantages of DHTML? Question 3 Explain the concept of DOM Question 4 How does AJAX work

Project , You get a contract to implement a simple Java application that pr...

You get a contract to implement a simple Java application that process NBA team roster : your application has to read the NBA team roster from a text file and then print each playe

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