Logical Student Language🔗ℹ

The Logical Student Language (LSL) is a teaching language that extends the Intermediate Student Language (ISL) from How to Design Programs with features that support formally reasoning about programs. In particular, LSL tightly integrates contracts and property-based randomized testing.

1 Inherited from ISL🔗ℹ

2 Extended from ISL🔗ℹ

• make-structure-name : takes a number of arguments equal to the number of fields in the structure, and creates a new instance of that structure.

• structure-name-field-name : takes an instance of the structure and returns the value in the field named by field-name.

• set-structure-name-field-name! : takes an instance of the structure and a value, and sets the field named by field-name in the given instance of the structure to the given value.

• structure-name? : takes any value, and returns #t if the value is an instance of the structure.

The name of the new functions introduced by define-struct must not be the same as that of other functions or variables, otherwise define-struct reports an error.

(define-struct posn [x y])

(define a-posn (make-posn 0 0))

(posn-x a-posn)

0

(define-mutable-struct box [value])

(define a-box (make-box 0))

(set-box-value! a-box 1)

(box-value a-box)

1

3 Testing🔗ℹ

4 Contracts🔗ℹ

(define-contract IntToInt   (-> Integer Integer))

(: on-two-and-three (-> (-> Integer Integer) Integer))

(define (on-two-and-three g)   (+ (g 2) (g 3)))

Uses of on-two-and-three are protected:

> (on-two-and-three (lambda (x) (* x x)))

13

> (on-two-and-three (lambda (x) (/ x 2)))

on-two-and-three: contract violation

expected: Integer

given: 3/2

blaming: program (as client)

4.1 Primitives🔗ℹ

syntax (check predicate-expr)

The predicate-expr is expected to produce a predicate that determines if a value satisfies the contract.

syntax (generate gen-expr)

The gen-expr should evaluate to a function that takes a single natural number, the fuel, and produces a value that satisfies the contract. Fuel provides a rough measure of how hard the generator is willing to work to produce a value.

syntax (feature name-string feature-expr)

The feature-expr function takes one argument, a value satisfying the contract. It then computes some property of that value for use in Tyche. An Immediate can have more than one feature.

syntax (shrink shrink-expr)

The shrink-expr function takes two arguments, fuel and a value to shrink. The value to shrink is guaranteed to satisfy the contract.

syntax (arguments [id contract] ...)

Describes the contracts on arguments. Any id can be used in any contract and will be bound to the concrete argument when the function is applied, so long as there is no cyclic dependency.

syntax (result contract)

Describes the result contract. All id values are available in contract.

syntax (raises exn-id)

Permits the exn-id struct to be raised in the function. Such exceptions are not considered failures during property-based testing.

4.2 Derived🔗ℹ

To use a Maybe value, you must check if the output is a Boolean with false?, or by using the contract for the associated type.

> (: bigger-than-three (-> Integer (Maybe Integer)))

> (define (bigger-than-three n)     (if (> n 3) n #f))

> (let ([x (bigger-than-three 1)])     (if (false? x) "small" x))

"small"

> (filter integer? (map bigger-than-three (list 1 2 3 4 5)))

'(4 5)

5 Property-Based Randomized Testing🔗ℹ

6 State Machines🔗ℹ

6.1 DFAs🔗ℹ

> (define M     (dfa s1 (s1)          [s1 ([0 s2]               [2 s1])]          [s2 ([0 s1]               [2 s2])]))

> (machine-accepts? M (list 2 0 2 0 2))

#t

> (machine-accepts? M (list 0 2 0 2 0))

#f

6.2 Regular Expressions🔗ℹ

> (define R (re (star (seq 'a 'b))))

> (machine-accepts? R (list 'a 'b 'a 'b))

#t

> (machine-accepts? R (list 'a 'b 'a))

#f

syntax literal

A literal value recognizes itself.

syntax (complement re)

Recognizes anything that is not recognized not re.

syntax (seq re ...)

Recognizes a sequence of regular expressions.

syntax (seq-prefix re ...)

Recognizes prefixes of the given regular expression. In other words, (seq-prefix x y z) is the same as (union (epsilon) x (seq x y) (seq x y z)).

syntax (union re ...)

Recognizes any of the given re.

syntax (star re)

Recognizes zero or more repetitions of re.

syntax (epsilon)

Recognizes the empty list.

7 Resources🔗ℹ

Outputs a visualization graphing how much time f takes for each of the given args.

8 Concurrency🔗ℹ

An actor system consists of a number of actors (or processes) that are identified by a unique name. Actors send immutable values (or messages) to one another. These messages are then processed by the receiving actor. Messages are guaranteed to be delivered in FIFO (first-in-first-out) between two actors. However, the order in which messages are delivered among all actors is unspecified. When starting an actor system, a scheduler can be provided to fix some delivery policy.

See start for an example of a concurrent system.

syntax (name s)

s   :   String

Names a process. This needs to be unique across all processes in a system.

syntax (on-start handler)

handler   :   (-> (List String) (Action contract))

The handler function is applied to the list of all the other processes (as strings) when the process starts. The result of the call is an action, containing the new state of the process and a list of packets to send to other processes.

syntax (on-receive handler)

handler   :   (-> contract ReceivePacket (Action contract))

The handler function is applied to the process’s state and a packet when the process receives a new packet. The result of the call is an action, containing the new state of the process and a list of packets to send to other processes.

The example below demonstrates a concurrent program with two processes, a and b, which send greetings back and forth. The program starts with a greeting b. Each process has its own state, remembering how many greetings it has sent so far. Once each process has sent three greetings, they stop greeting, and the concurrent program terminates.

(define MAX-GREETINGS 3)   (: a-receive (-> Natural (ReceivePacket String) (Action Natural))) (define (a-receive state pkt)   (cond     [(>= state MAX-GREETINGS) (action state (list))]     [else      (let ([new-state (add1 state)]            [messages-to-send (list (send-packet "b" "Hi b!"))])        (action new-state messages-to-send))]))   (: b-receive (-> Natural (ReceivePacket String) (Action Natural))) (define (b-receive state pkt)   (cond     [(>= state MAX-GREETINGS) (action state (list))]     [else      (let ([new-state (add1 state)]            [messages-to-send (list (send-packet "a" "Hi a!"))])        (action new-state messages-to-send))]))   (start first (list (process (name "a")                             (on-start (λ (others) (action 1 (list (send-packet "b" "Hi b!")))))                             (on-receive a-receive))                    (process (name "b")                             (on-start (λ (others) (action 0 (list))))                             (on-receive b-receive))))

'(("b" 3) ("a" 3))

The extra argument, summarize-state, is a function that is applied to the process state before it is displayed, since large process states can make the interface harder to use. The identity function can be provided if you want the entire process state visible.