From cb1ddbfa3f5d6594ec2538a633b35d269a6c2fa7 Mon Sep 17 00:00:00 2001 From: Grigore Rosu Date: Tue, 24 Oct 2023 12:24:01 -0500 Subject: [PATCH] Update index.md --- teaching/2023/cs422/index.md | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/teaching/2023/cs422/index.md b/teaching/2023/cs422/index.md index 878c4d6..4feb665 100644 --- a/teaching/2023/cs422/index.md +++ b/teaching/2023/cs422/index.md @@ -100,6 +100,26 @@ Note: See the [abort](https://github.com/runtimeverification/k/tree/master/k-dis - [K Tutorial, Part 5: Defining type systems](https://kframework.org/k-distribution/pl-tutorial/) (this is optional at this stage, but instructive for better understanding the static semantics; read at least Lesson 1, and skim Lesson 6). Click [here](https://github.com/kframework/k/tree/master/k-distribution/pl-tutorial/1_k/5_types) to see the code on GitHub. - [K Overview]({{site.baseurl}}/assets/CS422-K-Overview.pdf) paper, which also defines and explains SIMPLE. Sections 3 and 4 (the other sections were covered above) +--- +HW4 (due date: Friday, April 1st, AoE --- extended by 3 days to Monday, April 4th, AoE) + +***Exercise 1 (10 points):*** Add `break;` and `continue;` to untyped SIMPLE. Just take the semantics of these from C/C++/Java, if uncertain. Do only the simple, unlabeled ones, which only break/continue the innermost loop. One thing to think about: do you still want to desugar the for-loop into a while-loop as we do it now? + +Note: See the [break-continue](https://github.com/kframework/k/tree/master/k-distribution/pl-tutorial/2_languages/1_simple/1_untyped/exercises/break-continue) exercise for untyped SIMPLE in the nightly built for details and test programs. + +***Exercise 2 (10 points):*** Our current exceptions in SIMPLE are quite simplistic: the thrown exceptional value is caught by the innermost try-catch statement, and you get a runtime error (stuck) if the type of the thrown value is not the same as the type of the exception's parameter. They work fine if you restrict them to only throw and catch integer values, like we did in the static semantics, but modern languages do not like this limitation. Change the existing dynamic semantics of typed SIMPLE to propagate a thrown exception to the outer try-catch statement when the inner one cannot handle the exception due to a type mismatch. For example, `try { try { throw 7; } catch(bool x) {print(1};} } catch{int x) {print(2);}` should print 2, not get stuck as it currently happens. + +Note: See the [typed-exceptions](https://github.com/kframework/k/tree/master/k-distribution/pl-tutorial/2_languages/1_simple/2_typed/2_dynamic/exercises/typed-exceptions) exercise for dynamically typed SIMPLE in the nightly built for details and test programs. + +***Exercise 3 (10 points):*** Same as Pb2, but for the static semantics of the typed SIMPLE. For this exercise (but not for the previous one), modify also the syntax of SIMPLE to allow functions to declare what exceptions they can throw. + +Note: See the [functions-with-throws](https://github.com/kframework/k/tree/master/k-distribution/pl-tutorial/2_languages/1_simple/2_typed/1_static/exercises/functions-with-throws) exercise for statically typed SIMPLE in the nightly built for details and test programs. + +***Exercise 4 (10 points):*** Compilers typically collect all the variables declared in a block and move them all in one place, renaming them appropriately everywhere to avoid name conflicts. Consequently, they do not like you to declare a variable twice in the same block. Modify the static semantics of SIMPLE to reject programs which declare the same variable twice in a block. Your resulting type system should get stuck when a variable is declared the second time. + +Note: See the [no-duplicate-declarations](https://github.com/kframework/k/tree/master/k-distribution/pl-tutorial/2_languages/1_simple/2_typed/1_static/exercises/no-duplicate-declarations) exercise for statically typed SIMPLE in the nightly built for details and test programs. + +For each of the problems, also provide one test program which should succeed and one which should fail. You will get two extra-points if any of your tests break everybody's definition (except potentially yours). If you handle more than one succeeding and one failing test, then I will randomly choose one of each. --- ... more to come ...