Question $2.(20$ pts$.)$ Consider the following set of pre and postconditions for a method:

$//$ Precondition: "letter" is a character from the set

$//$ of characters defined by the following ranges:

$//\text{'}$A$\text{'}...\text{'}$Z$\text{'},\text{'}$a$\text{'}...\text{'}$z$\text{'},\text{'}0\text{'}...\text{'}9\text{'}$

$//$

$//$ Postcondition: The value returned by the function

$//$ is true if "letter" is a letter of the English alphabet;

$//$ otherwise the value returned by the function is false.

boolean is$\_$alpha$($char letter$)\{$

$...//$ Implementation of is$\_$alpha$()$

$\}$

What is the result of the following call:

is$\_$alpha$(\text{'}!\text{'})$;

Select the best option:

$($a$)$ true

$($b$)$ false

$($c$)$ null

$($d$)$ The result is undetermined

$($e$)$ An exception is thrown

$($f$)$ Code that calls is$\_$alpha$()$ would not compile.

$($g$)$ None of the aboveQuestion $3.(20$ pts$.)$ A Hoare triple which is true would still be true if we replace the precondition with true.

$($a$)$ true

$($b$)$ false

Question $4.(20$ pts$.)$ Indicate whether the following statements are true or not and provide a brief explanation why.

$($a$)$ If Dafny successfully verified your code, it means that your code has no bugs.

$($b$)$ If Dafny returned an error when verifying your code, it means that your code has a bug.