Logical Student Language

8.12

Logical Student Language🔗ℹ

Cameron Moy

Daniel Patterson

package: lsl-lib

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, property-based randomized testing, and symbolic execution.

1 Inherited from ISL🔗ℹ

Syntax	..., and, cond, define, else, if, lambda, let, let*, letrec, local, or, quote, require, λ
Testing	check-error, check-expect, check-member-of, check-random, check-range, check-satisfied, check-within
Equality	eq?, equal?
Booleans	boolean=?, boolean?, false, not, true
Numbers	*, +, -, /, <, <=, =, >, >=, abs, add1, ceiling, even?, exact->inexact, expt, floor, inexact->exact, integer?, max, min, modulo, negative?, number?, odd?, pi, positive?, quotient, random, real?, remainder, sgn, sqr, sqrt, sub1, zero?
Strings	format, list->string, make-string, string, string->list, string->number, string->symbol, string-append, string-contains?, string-copy, string-downcase, string-length, string-ref, string-upcase, string=?, string?, substring
Lists	append, assoc, assq, build-list, car, cdr, cons, cons?, eighth, empty, empty?, fifth, first, fourth, length, list, list-ref, list?, member?, memq, memq?, null, null?, remove, rest, reverse, second, seventh, sixth, third
Functions	andmap, apply, argmax, argmin, compose, filter, foldl, foldr, for-each, identity, map, memf, ormap, procedure?, sort

2 Extended from ISL🔗ℹ

syntax
(define-struct structure-name (field-name ...))

Defines a new structure called structure-name. The structure’s fields are named by the field-names. After the define-struct, the following new functions are available:

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))
(set-posn-x! a-posn 1)
(posn-x a-posn)
1

syntax
(begin expr0 ... expr)

Executes the given expressions in sequence, returning the last expr.

syntax
(set! id expr)

Mutates the variable id with the value of expr.

3 Testing🔗ℹ

syntax
(test-suite "name" ...)

Declares a named block of tests. Aside from printing and for autograding, no different from putting check-expect or similar at the top-level.

4 Contracts🔗ℹ

syntax
(define-contract id contract)

Creates id as an alias for contract.

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

syntax
(: id contract)

Annotates id with a contract. When id is created with define, the contract is attached to the defined value.

(: 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
(Immediate clause ...)

An immediate contract is one that can be checked immediately, without imposing any future checks. As a shorthand, an ordinary LSL expression e in a contract position is automatically converted to the immediate contract (Immediate (check e)).

(define-contract Even
  (Immediate (check (lambda (x) (and (integer? x) (even? x))))
             (generate (lambda (fuel) (* 2 (random (add1 fuel)))))
             (shrink (lambda (fuel x)
                       (let ([y (/ x 2)])
                         (if (even? y) y (sub1 y)))))
             (symbolic (lambda () (* 2 (contract-symbolic Integer))))))

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
(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
(symbolic sym-expr)
The sym-expr function takes no arguments and produces a symbolic value that represents all values that satisfy the contract.

syntax
(Function clause ...)

A function contract protects a function by constraining its inputs and outputs. Arguments are labeled so that dependent properties can be checked.

(: double (Function (arguments [x Integer])
(result (lambda (y) (= x y)))))
(define (double x)
(* 2 x))

The double function violates this contract:

> (double 0)
0
> (double 1)
double: contract violation
  expected: (lambda (y) (= x y))
  given: 2
  blaming: program (as server)

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 and symbolic execution.

syntax
(List contract)

Describes a list of arbitrary length whose elements satisfy contract.

> (contract-generate (List Integer))
'(-44)

syntax
(Tuple contract ...)

Describes lists where the k-th element satisfies the k-th contract. The list must have exactly the same number of elements as there are contracts.

> (contract-generate (Tuple Boolean Integer))
'(#f -21)

syntax
(OneOf contract ...)

A value satisfying a OneOf contract must satisfy exactly one of the given contracts.

> (contract-generate (List (OneOf Boolean Integer)))
'(35
  -31
  -22
  #f
  45
  #f
  #t
  #f
  #f
  #f
  23
  13
  #t
  #t
  4
  -38
  1
  #f
  #t
  #t
  -49
  #f
  #f
  15
  #t
  #f
  -20
  #t
  19
  #f
  #f
  -15
  -39
  -34
  #f
  #f
  25
  -48
  #t
  #t
  -47
  #t
  -3
  #f
  #f
  #f)

syntax
(AllOf contract ...)

A value satisfying an AllOf contract must satisfy all of the given contracts.

> (define-contract UnitInterval
    (AllOf Real
           (lambda (x) (< 0 x))
           (lambda (x) (< x 1))))
> (: reciprocal (-> UnitInterval Real))
> (define (reciprocal x) (/ 1 x))
> (reciprocal 1/2)
2
> (reciprocal -2)
reciprocal: contract violation
  expected: (lambda (x) (< 0 x))
  given: -2
  blaming: program (as client)
> (reciprocal 2)
reciprocal: contract violation
  expected: (lambda (x) (< x 1))
  given: 2
  blaming: program (as client)

syntax
(Struct struct-id (field-contract ...))

Struct contracts describe each individual field on the struct. Each struct definition automatically generates a shorthand for such a contract, as such:

> (define-struct my-point (x y))
> (contract-generate (MyPoint Integer Integer))
(make-my-point -12 0)

syntax
(All (id ...) contract)

A universal contract that guarantees id is used uniformally within contract. This form is often used to define parametrically polymorphic functions.

> (: id (All (A) (-> A A)))
> (define (id x) x)
> (id 10)
10

syntax
(Exists (id ...) contract)

An existential contract that guarantees id is used uniformally within contract. This form is often used for data abstraction.

> (: counter-pkg (Exists (A) (Tuple (-> A) (-> A A) (-> A Integer))))
> (define counter-pkg
    (list (λ () 0)
          (λ (x) (+ x 1))
          (λ (x) x)))
> (define make-counter (first counter-pkg))
> (define counter-incr (second counter-pkg))
> (define counter-get (third counter-pkg))
> (counter-get (counter-incr (make-counter)))
1

4.2 Derived🔗ℹ

syntax
Any
syntax
True
syntax
False
syntax
Boolean
syntax
Natural
syntax
Integer
syntax
Real
syntax
String
syntax
Symbol

Atomic contracts that recognize their respective types.

syntax
(Constant expr)

Only values equal? to expr are permitted.

syntax
(Maybe contract)

Either #f or a value satisfying the specified contract.

syntax
(-> arg-contract ... result-contract)

A shorthand for a Function contract with no dependencies.

syntax
(Record maybe-folding trace-id)

maybe-folder =
| folding-expr

The name of this contract rhymes with sword since the contract records values in a trace.

Uses the folding function folding-expr to integrate values that pass through the contract into the value at trace-id. The folding function takes two arguments: the current value of trace-id and the contracted value.

> (: down-prev (Maybe Natural))
> (define down-prev #f)
> (: down-folder (-> (Maybe Natural) Natural Natural))
> (define (down-folder prev cur)
    (cond
      [(equal? prev cur) #f]
      [else cur]))
> (: down (-> (AllOf Natural (Record down-folder down-prev))))
> (define down
    (let ([x 3])
      (lambda ()
        (begin
          (set! x (if (< x 1) 0 (sub1 x)))
          x))))
> (down)
2
> (down)
1
> (down)
0
> (down)
down-folder: contract violation
  expected: Natural
  given: #f
  blaming: program (as server)

If no folding function is provided, values will be appended to the end of list at trace-id.

> (define-contract Increasing
    (AllOf (List Real)
           (lambda (xs) (equal? (sort xs <) xs))))
> (: up-results Increasing)
> (define up-results '())
> (: up (-> (AllOf Natural (Record up-results))))
> (define up
    (let ([x 0])
      (lambda ()
        (begin
          (set! x (modulo (add1 x) 4))
          x))))
> (up)
1
> (up)
2
> (up)
3
> (up)
contract violation
  expected: (lambda (xs) (equal? (sort xs <) xs))
  given: '(1 2 3 0)

5 Property-Based Randomized Testing🔗ℹ

syntax
(check-contract id maybe-attempts)

maybe-attempts =
| nat-expr

Attempts to break the contract placed on id by randomly generating inputs. The number of times it attempts to do so is controlled by maybe-attempts.

> (: bigger-even (-> Integer Even))
> (define (bigger-even x)
    (* 3 x))
> (check-contract bigger-even 20)
--------------------
ERROR
params:     '(#<procedure:...yntax/interface.rkt:83:7> 20)
name:       check-contract
location:   eval:56:0
read-solution: unrecognized solver output: #<eof>
--------------------

syntax
(contract-generate contract maybe-fuel)

maybe-attempts =
| nat-expr

Generates a value that satisfies the given contract using the supplied fuel.

> (contract-generate Even)
82

6 Verification via Symbolic Execution🔗ℹ

syntax
(verify-contract id)

Similar to check-contract, except it uses symbolic execution try and break the contract.

> (: usually-fine (-> Integer Even))
> (define (usually-fine x)
    (if (= x 1000) 17 (* 2 x)))
> (verify-contract usually-fine)
--------------------
ERROR
params:     '(#<procedure:...yntax/interface.rkt:83:7>)
name:       verify-contract
location:   eval:60:0
read-solution: unrecognized solver output: #<eof>
--------------------

syntax
(contract-symbolic contract)

Returns a symbolic value that represents all values satisfying the given contract.

> (contract-symbolic Even)
(* 2 x$1)

7 State Machines🔗ℹ

procedure
(machine? x) → boolean?
x : any/c

Identifies machines.

procedure
(machine-accepting? x) → boolean?
x : any/c

Identifies accepting machines.

procedure
(machine-accepts? m l) → boolean?
m : machine?
l : list?

Returns #t if m ends in an accepting state after consuming every element of l.

procedure
(machine-next m x) → machine?
m : machine?
x : any/c

Produces a machine starting from m and consuming x.

7.1 DFAs🔗ℹ

syntax
(dfa start
     (end ...)
     [state ([in next-state] ...)]
     ...)

Returns a deterministic finite automaton (DFA) that starts in state start and where each state behaves as specified in the rules.

> (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

7.2 Regular Expressions🔗ℹ

syntax
(re re-form)

Returns a machine that recognizes the given regular expression.

> (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.

8 Resources🔗ℹ

procedure
(ticks thunk) → integer?
thunk : (-> any/c)

Returns a unitless quantity that represents how much "time" it takes to execute thunk.

procedure
(visualize args f) → any/c
args : list?
f : (-> any/c any/c)

To use this, (require lsl/performance).

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

9 Concurrency🔗ℹ

Concurrency is not the same as parallelism. In parallelism, computations occur simultaneously, not just in an arbitrary order.

A concurrent system is one in which the order of computations occur may vary. There are many models of concurrency, but the one supported by LSL is based on the actor model.

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.

syntax
(Packet contract)

Describes a packet sent from a process identified by a String, sent to a process identified by a String, and containing a message that satisfies contract.

procedure
(packet-from p) → String
p : (Packet Any)

Extracts an identifier representing the process (or actor) that a packet was sent from.

procedure
(packet-to sp) → String
sp : (Packet Any)

Extracts an identifier representing the process (or actor) that a packet was sent to.

procedure
(packet-msg sp) → Any
sp : (Packet Any)

Extracts the message (data) from a packet.

procedure
(packet? x) → Boolean
x : Any

Determines if its input is a packet.

syntax
(SendPacket contract)

Describes a packet to send to a process identified by a String and containing a message that satisfies contract.

(: sp (SendPacket Natural))
(define sp (send-packet "process-1" 42))

procedure
(send-packet to msg) → (SendPacket Any)
to : string?
msg : any/c

A packet to be sent to process to with message msg.

procedure
(send-packet-to sp) → String
sp : (SendPacket Any)

Extracts an identifier representing the process (or actor) that a packet should be sent to.

procedure
(send-packet-msg sp) → Any
sp : (SendPacket Any)

Extracts the message (data) from a packet to be sent.

procedure
(send-packet? x) → Boolean
x : Any

Determines if its input is a packet to be sent.

syntax
(ReceivePacket contract)

Describes a packet received from a process identified by a String containing a message that satisfies contract.

(: rp (ReceivePacket Natural))
(define rp (receive-packet "process-1" 42))

procedure
(receive-packet from msg) → (ReceivePacket Any)
from : string?
msg : any/c

A packet that was sent from process from with message msg.

procedure
(receive-packet-from rp) → String
rp : (ReceivePacket Any)

Extracts an identifier representing the process (or actor) that a packet was sent from.

procedure
(receive-packet-msg rp) → Any
rp : (ReceivePacket Any)

Extracts the message (data) from a received packet.

procedure
(receive-packet? x) → Boolean
x : Any

Determines if its input is a received packet.

syntax
(Action contract)

Describes an action containing a new state that satisfies contract and a list of packets to send satisfying (List (SendPacket Any)).

(: a (Action Natural))
(define a (action 5 (list (send-packet "process-1" 42)
(send-packet "process-1" 43)
(send-packet "process-2" "Hello!"))))

procedure
(action state packets) → (Action Any)
state : Any
packets : (List (SendPacket Any))

The result of a process handler: combines the updated process state and a list of packets to send (which may be empty). The list of packets is sorted (per process) from earliest to latest. In the example above, process-1 is guaranteed to receive the 42 packet before it receives the 43 packet. However, the relative order the packets are received among different processes is unknown a priori (as it is determined by the scheduler).

syntax
Process

A contract for a process.

syntax
(process clause ...)

clause = (name s)
| (on-start handler)
| (on-receive handler)

Defines a process that represents a single actor in a concurrent system. All of the clauses of a process description are mandatory.

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.

procedure
(start scheduler processes) → (List (Tuple String Any))
scheduler : (-> (List (Packet Any)) (Packet Any))
processes : (List Process)

Runs a concurrent program using a fixed list of processes. When no more messages need to be processed, the function returns a list of pairs of the process name and final state.

procedure
(start-debug scheduler processes) → (List (Tuple String Any))
scheduler : (-> (List (Packet Any)) (Packet Any))
processes : (List Process)

Like start, but prints to the interactions window as each message is received and what the corresponding process state updates to.

procedure
(start-gui scheduler
processes
summarize-state) → (List (Tuple String Any))
  scheduler : (-> (List (Packet Any)) (Packet Any))
  processes : (List Process)
  summarize-state : (-> Any Any)

Like start, but runs the program in an interactive graphical interface instead. The interface allows you to step forward and backward through the program, viewed through either a graph showing the current packet being sent/received, a table of the current messages waiting to be processed, or a history of all process states up to the current moment.

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.

1	Inherited from ISL
2	Extended from ISL
3	Testing
4	Contracts
5	Property-Based Randomized Testing
6	Verification via Symbolic Execution
7	State Machines
8	Resources
9	Concurrency