CSE4250/Stansifer

Final (with solutions)

Summer 2021

1. (50 points).

The following program is written in the simple while language used in class. Formalize in first-order logic something useful that the program accomplishes. Using the five rules of inference used in class prove that the program accomplishes what you say.

i := 1; s := 0;

while i <= n do

    j := 1;

    while j <= i do

        s := s + j;

        j := j + 1

    od ;

    i := 1 + 1

od

Your answer will be evaluated based on these criteria:

• The formalization of correctness

• The expressiveness of correctness

• The correct application of the rules

• The presentation of the proof

2. (50 points).

Write a brief research survey paper on subtyping of function types. Your survey must include some of the programming languages Kotlin, Scala, Java, C#, Dart, OCaml. You must have examples and references to definitive sources. The references must not be Wikipedia, StackOverflow, Rosetta Code and the like. However, you may take examples from these sources, if you cite them.

Specifically, your paper must address two issues:

• where in a programming language the covariant, contravariance, or invariance of a function matters, and

• what flexibility (polymorphism) does the language permit.