Assignment 4 (Written, Tool):Hoare Logic and Spec#17-654/17-754: Analysis of Software ArtifactsJonathan Aldrich ([email protected])Due: Thursday, February 22, 2007 (10:30am)150 points totalTurn in a file named <username>-17654-A4.zip, where username isyour Andrew id. This zip file should contain answers.{txt, pdf, doc} whichshould contain your responses to each of the written questions. The zip fileshould also contain Stack.ssc, stack-output.txt, Min.ssc and min-output.txtwhich are described in the following sections. At the top of the answers file,state your name, Andrew id, and how long you spent on the assignment.Assignment Objectives:• Become familiar with specification constructs including pre- and post-conditions, loop invariants and variant functions• Prove small programs correct using Hoare logic techniques• Use Spec# to check functional correctness properties of programs11 Hoare Logic (50 points)Question 1 (10 points).Consider the following WHILE program:i := 1;r := 1;while (i < n) doi := i + 1;r := r + iFor the while program given above, state a (a) precondition, (b)postcondition, (c) loop invariant, and (d) variant function. Thepostcondition should precisely define the value of r in terms ofn.Question 2 (30 points).Using weakest preconditions, state the proof obligations that as-sure (a) the invariant is initially true on entry to the loop, (b) theloop invariant holds after execution of each loop, (c) the vari-ant function is greater than zero at loop entry, (d) the variantfunction decreases in the loop, and (e) the postcondition holds.Question 3 (10 points).Prove each of the proof obligations above. Your proof shouldbe done at the level of detail shown in lecture, i.e. small stepswith justifications given for each step.22 Using Spec# (100 points)Question 4 (60 points).For this assignment you will be required to use the Microsoft VisualStudio environment. Visual Studio 2005 works. Visual Studio 2003 shouldwork, but you should consider it unsupported for the purposes of thiscourse. If you do not currently have Visual Studio, you are all able to obtainit through ISR. According to Ed Walter, you have all received instruction onhow to download and install the software that is provided as part of the Mi-crosoft Academic Alliance. If you have trouble with this, please see him forassistance. If you do not use a Windows-compatible PC, it will be necessaryto obtain access to one for this assignment. The clusters are a good placefor this. All instructions from here on assume that you have Visual Studioinstalled.Installing Spec# and the Simplify Theorem Prover: In order to installSpec#, start by visiting the Spec# homepage:http://research.microsoft.com/specsharp/From here you will be able to install Spec# for VS2005. Do not use theVS2003 version of Spec#. Additionally, you must install the Simplify theo-rem prover. Instructions on this process are given at the following URL:http://research.microsoft.com/specsharp/simplify.htmFrom within Visual Studio, open the project Stack that we have in-cluded with the assignment. This project contains C# source files, Stack.sscand StackCheck.ssc. The Spec# static verifier should be run automaticallyin the background. Any warnings that it finds will be printed to the “Er-ror List” window. (If this window is not visible, enable it via the “View”menu.) The output of the static verifier can also be seen in the “Output”window, and you will need to have this window visible so that can copythe tool’s output and submit it.Add pre- and post-conditions and invariants to Stack.ssc and fix anybugs you find in the code, until Spec# runs on both files without producingany warnings. You may not edit StackCheck.ssc. Nor may you remove theannotations that are already present in Stack.ssc.(To learn more about the specifications that you can use in Spec# wehave included some documentation in a file called “specsharpdocs.html.”The installation of Spec# includes sample files which may also be helpful.Finally, additional documentation can be found on the Spec# web site.)Turn in: (a) your edited version of Stack.ssc, and (b) a printout of Spec#’soutput when run on the two files in stack-output.txt.3Question 5 (30 points).Write a method that returns the minimum integer in a given array. Thismethod should have the following signature:public int findMin(int[]! array);Check the correctness of this method using the Spec# static verifier, i.e.that it really finds the minimum value. Your solution should use appropri-ate requires, ensures, and invariant clauses.Turn in: (a) your C# code Min.ssc, and (b) a printout of Spec#’s outputwhen run on the Min.ssc in min-output.txt.Question 6 (10 points).In the file answers.txt, criticize the Spec# static verifier tool (1-2 para-graphs). What did you like about it, and conversely what stands in theway of making this a practical