Ask Automata & Computation Expert

Question 1

Hoare Logic Semantics

For each of the parts below, justify your answer briefly.
1. For which programs S does {False} S {True} hold?
2. For which programs S does {True} S {False} hold?
3. For which programs S does [True] S [True] hold?

Question 2

Doubling Numbers

The following piece of code is called Half:
x := 0;
y := 0;
while (x < a)
x := x + 2; y := y + 1;

We wish to use Hoare Logic to show that:

{True} Half {x = 2 ∗ y}

In the questions below (and your answers), we may refer to the loop code as Loop, the body of the loop (i.e. x:=x+2;y:=y+1;) as Body, and the initialisation assignments (i.e. x:=0;y:=0;) as Init.

1. Given the desired postcondition {x = 2 ∗ y}, what is a suitable invariant for Loop? (Hint: notice that the postcondition is independent of the value of a.)

2. Prove that your answer to the previous question is indeed a loop invariant. That is, if we call your invariant P , show that {P } Body {P }. Be sure to properly justify each step of your proof.

3. Using the previous result and some more proof steps show that

{True} Half {x = 2 ∗ y}
Be sure to properly justify each step of your proof.

4. To prove total correctness of the program Half, identify and state a suitable variant for the loop. Using the same invariant P as above, the variant E should have the following two properties:

- it should be ≥ 0 when the loop is entered, i.e. P ∧ (x < a) → E ≥ 0
- it should decrease every time the loop body is executed, i.e. [P ∧ (x < a) ∧ E = k] Body [P ∧ E < k] 1

You just need to state the variant, and do not need to prove the two bullet points above (yet).

5. For the variant E you have identified above, give a proof of the premise of the while-rule for total correctness, i.e. give a Hoare-logic proof of [P ∧ (x < a) ∧ E = k] Body [P ∧ E < k] and argue that P ∧ (x < a) → E ≥ 0.

Question 3

Counting Modulo 7

Consider the following code fragment that we refer to as Count below, and we refer to the body of the loop (i.e. the two assignments together with the if-statement) as Body.

while (y < n)
y := y + 1; x := x + 1;
if (x = 7) then x := 0 else x := x

The goal of the exercise is to show that {x < 7}Count{x < 7}

1. Given the desired postcondition, what is a suitable invariant P for the loop? You just need to state the invariant.

2. Give a Hoare Logic proof of the fact that your invariant above is indeed an invariant, i.e. prove the Hoare-triple {P }Body{P }.

3. Hence, or otherwise, give a Hoare-logic proof of the triple {x < 7}Count{x < 7}.

4. Give an example of a precondition P so that the Hoare-triple {P }Count{x < 7} does not hold and justify your answer briefly.

Attachment:- Appendix.rar

Automata & Computation, Computer Science

  • Category:- Automata & Computation
  • Reference No.:- M93126815
  • Price:- $70

Guranteed 36 Hours Delivery, In Price:- $70

Have any Question? 


Related Questions in Automata & Computation

Solve the question given belowprove the following statement

Solve the question given below Prove the following statement using Hall's Theorem. For any bipartite graph G=(U, V, E), if every node (either a left node or a right node) has exactly d neighbors, where d is an arbitrary ...

Prove or disprove the following proposed inference rules

Prove or disprove the following proposed inference rules for functional dependencies. A proof should be made by using the reflexive, augmentation, transitive, decomposition, union, and pseudotransitive rules. A disproof ...

Prove or disprove the following proposed inference rules

Prove or disprove the following proposed inference rules for functional dependencies. A proof should be made by using the reflexive, augmentation, transitive, decomposition, union, and pseudotransitive rules. A disproof ...

Iot and data analytics1 analyse the taskanalyse what is

IOT and data analytics 1. Analyse the Task Analyse what is expected of you. This includes careful reading of the assignment task as specified in the Subject Outline. The executive summary of the research project is to be ...

Question 1a digital computer has a memory unit with 16 bits

Question 1: A digital computer has a memory unit with 16 bits per word. The instruction set consists of 122 different operations. All instructions have an operation code part (opcode) and an address part (allowing for on ...

Regular expressions automatacomputabilitytheory of

Regular expressions, automata/computability/theory of computation How would I go about interpreting regular expressions? For example, how would I interpret the following in English: (0+1)*011 0*1*2* 0^(+)1^(+)2^(+)

Models of computation assignment -purpose - to improve and

Models of Computation Assignment - Purpose - To improve and consolidate your understanding of regular and context-free languages, finite-state and pushdown automata. To develop skills in analysis and formal reasoning abo ...

Models of computation assignment -purpose - to improve and

Models of Computation Assignment - Purpose - To improve and consolidate your understanding of regular and context-free languages, finite-state and pushdown automata. To develop skills in analysis and formal reasoning abo ...

Question - design a state machine that will control a

Question - Design a state machine that will control a vending machine. The vending machine has 4 inputs, N, D indicating a nickel or dime was inserted as well as clk and an active high asynchronous reset. The vending mac ...

Question - design a task or function that will check the

Question - Design a task or function that will check the parity of a word for odd parity. The input to the task/function is a 5-bit word called data_in. If the parity of input data_in is not odd increment an error count ...

  • 4,153,160 Questions Asked
  • 13,132 Experts
  • 2,558,936 Questions Answered

Ask Experts for help!!

Looking for Assignment Help?

Start excelling in your Courses, Get help with Assignment

Write us your full requirement for evaluation and you will receive response within 20 minutes turnaround time.

Ask Now Help with Problems, Get a Best Answer

Why might a bank avoid the use of interest rate swaps even

Why might a bank avoid the use of interest rate swaps, even when the institution is exposed to significant interest rate

Describe the difference between zero coupon bonds and

Describe the difference between zero coupon bonds and coupon bonds. Under what conditions will a coupon bond sell at a p

Compute the present value of an annuity of 880 per year

Compute the present value of an annuity of $ 880 per year for 16 years, given a discount rate of 6 percent per annum. As

Compute the present value of an 1150 payment made in ten

Compute the present value of an $1,150 payment made in ten years when the discount rate is 12 percent. (Do not round int

Compute the present value of an annuity of 699 per year

Compute the present value of an annuity of $ 699 per year for 19 years, given a discount rate of 6 percent per annum. As