10 Homework 12

In this assignment, you will be able to use any programming language you would like. If the only languages you know are ISL-Spec and Lean, you should use Racket (put #lang racket at the top of the file in DrRacket): it is not quite the same as ISL-Spec, but close enough to work. In that case, you can use the Racket Quickcheck library (by (require quickcheck)), which we used with ISL-Spec, and the Racket JSON library (by (require json)). You can install json from File->Install Package in DrRacket.

Step 1: Choose a programming language of your choice. It must have a property-based testing library, which you should find. For example, in Python, the best-supported library is Hypothesis. For Java, a quick search finds jqwik. For Javascript/Typescript, the first research of a search is "fast-check", etc.

10.1 Problem 1

Test out your property-based testing library by implementing the following functionality in your language, writing property-based tests, and running them:

1. Show that sorting a collection (array, list, etc) does not change the size of the collection.

2. Write code that adds an element to a collection (array, list, etc), if it doesn’t already exist in it, and show that it does not decrease the size of the collection.

10.2 Problem 2

In this problem, we want you to use an existing JSON serialization/deserialization library (if your language does not have one, you can of course implement it, but that’s not our intention).

First, you need to define a data structure (in your programming language) that represents a map from student ids (as strings) to structures representing students (with a name, list of interests, and address). This data structure is part of a hypothetical application for matching students with people who live near them and have similar interests, the rest of the application will not be implemented!

Now, you should write code that turns that data structure into JSON (using whatever functionality is available in your language’s JSON library), and separate code that does the reverse. This would be used to either store the data, or send it over the network.

Now, write property-based tests that show that for random examples of your data structure, the serialization and deserialization functions are inverses of each other; i.e., that deserialize(serialize(x)) = x for all x.

10.3 Problem 3

In this problem, first define a native data type for a color, which should be able to represent colors in the following three ways:

1. Named colors (Red, Green, Blue, etc: how many is up to you, but a finite number)

2. RGB colors (three numbers, 0 to 254, that represent the amount of Red, Green, or Blue in the color)

3. CMYK (four numbers, 0 to 254, that represent how much Cyan, Magenta, Yellow, and Black, in the color)

Now, write code that turns your color into a "packed" representation as an array (or list) of numbers. You are welcome to choose any representation as you like, but we’d suggest using the first number as a "tag" that indicates which possibility you are in.

Next, write code that takes a "packed" representation as an array (or list) of numbers, and convert it back into the native color data structure.

Finally, write property based tests that show that for random examples of your color, the "unpacking" and "packing" functions are inverses of each other; i.e., that unpack(pack(x)) = x for all x. You should also show that for any array (or list) of numbers, the "unpacking" function either gives a sensible error, or returns a color that, when "packed", gives the same array (or list) of numbers.