Identify and state a suitable variant for the loop

Assignment Help Theory of Computation
Reference no: EM132139350

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

Reference no: EM132139350

Questions Cloud

Write two relational algebra expressions : IT244 nderline the appropriate primary keys/foreign keys in the above relations. Write two relational algebra expressions that retrieve.
Should you trust a 3rd-party vendor to handle your backups : Should you trust a 3rd-party Vendor to handle your backups (cloud), or should you do it yourself in-house (on premises)? Why?
How many transactions in this market basket : ITS-632: What items represent Itemset (I)? How many transactions in this market basket? What is the support? What is the confidence?
Calculate increase or decrease in monthly operating income : Question - Calculate the increase or decrease in Boundaries' monthly operating income during 20x5 if the mall store is closed
Identify and state a suitable variant for the loop : 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 }
International business environment : Share an example of an ethical dilemma that can occur within the international business environment. Do not repeat examples from the textbook.
Theories of international trade and investment : Articulate the theories of international trade and investment . Give an example of one of the theories.
What is your reaction to harriets suggestion of using debt : Based on the materials presented in the "Risk and Return" video, present a discussion on why the materials are important in financial decision making.
What are the responsibilities of the internal auditors : CASE STUDY - FINANCIAL REPORT ANALYSIS - What are the responsibilities of the Internal Auditors? Have you identify any problem with this company

Reviews

Write a Review

Theory of Computation Questions & Answers

  Finite-state machine design

Create a finite-state machine design to turn your FPGA development board into a simple programmable music box.

  Redundant sequence identi cation

Redundant sequence identi cation

  Compute a shortest superstring

Dynamic programming algorithm to compute a shortest superstring.

  Propositional and predicate logic

Write down a structural induction principle for the PlayTree free type

  Design a syntactic analyzer

Design a syntactic analyzer for the language specified by the grammar

  Design unambiguous grammar to parse expressions

Write a program would read two numbers and then print all numbers between the first and the second, inclusive. Design unambiguous grammar to parse expressions

  Consider a logic function with three outputs

Consider a logic function with three outputs,  A ,  B , and  C , and three inputs,  D ,  E , and  F . The function is defined as follows:  A  is true if at least one input is true,  B  is true

  Considering a single programmed operating system

Considering a single programmed operating system, what is the minimal total time required to complete executions of the two processes? You should explain your answer with a diagram.

  How to construct an nfa

Give a construction that assumes you are given a DFA for L and show how to construct an NFA (with or without ε-moves) to recognize sort(L).

  Equivalence classes to construct minimal dfa for language

How many equivalence classes does this relation have and what are they? Use these equivalence classes to construct the minimal DFA for the language.

  Impact of moore-s law on data center costs

Discuss the impact of Moore's law on data center costs on such things as servers and communications equipment. List at least 3 steps or recommendations your data center can take to offset some or all of the effect of Moore's law.

  Problem encountered in statements in predicate logic

How the problem would be encountered in attempting to represent the following statements in Predicate logic. it should be possible to: John only likes to see French movies.

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