In this first lab, you will use Stainless (https://github.com/epfl-lara/stainless) to verify programs.

Install the latest release of Stainless (v0.7.3 at the time of the writing). The release is an archive containing among other things a binary called stainless, that you should make available in your path. Instructions are available in this short video. Make sure that you are using Java 8 (there might be issues with other versions of Java). On some Linux distributions, you can use sudo update-alternatives –config java to change versions.

As Stainless currently does not work out of the box on Windows, we advise you to run it with either the Windows Subsystem for Linux or a virtual machine running Linux. It may also work with something like Cygwin but this has not been tested yet.

Upload your solutions on Moodle by ?? at 23:59.

The code below defines a relation on lists, which holds when the first list can be embedded in the second list. The goal is to prove basic properties on this relation, such as reflexivity, transitivity, and antisymmetry. More precisely, you should make Stainless accept the seven lemmas defined in the code.

To familiarize yourself with Stainless, you can have a look at this tutorial:

• Part 1/4 (the installation video linked above)
• Part 2/4
• Part 3/4
• Part 4/4

import stainless.collection._
import stainless.lang._
import stainless.annotation._
 
object SubList {
 
  def subList[T](l1: List[T], l2: List[T]): Boolean = (l1, l2) match {
    case (Nil(), _)                 => true
    case (_, Nil())                 => false
    case (Cons(x, xs), Cons(y, ys)) => (x == y && subList(xs, ys)) || subList(l1, ys)
  }
 
  def subListRefl[T](l: List[T]): Unit = {
 
  }.ensuring(_ =>
    subList(l, l)
  )
 
  def subListTail[T](l1: List[T], l2: List[T]): Unit = {
    require(!l1.isEmpty && subList(l1, l2))
 
  }.ensuring(_ =>
    subList(l1.tail, l2)
  )
 
  def subListTails[T](l1: List[T], l2: List[T]): Unit = {
    require(!l1.isEmpty && !l2.isEmpty && l1.head == l2.head && subList(l1, l2))
 
  }.ensuring(_ =>
    subList(l1.tail, l2.tail)
  )
 
  def subListTrans[T](l1: List[T], l2: List[T], l3: List[T]): Unit = {
    require(subList(l1, l2) && subList(l2, l3))
 
  }.ensuring(_ =>
    subList(l1, l3)
  )
 
  def subListLength[T](l1: List[T], l2: List[T]): Unit = {
    require(subList(l1, l2))
 
  }.ensuring(_ =>
    l1.length <= l2.length
  )
 
  def subListEqual[T](l1: List[T], l2: List[T]): Unit = {
    require(subList(l1, l2) && l1.length >= l2.length)
 
  }.ensuring(_ =>
    l1 == l2
  )
 
  def subListAntisym[T](l1: List[T], l2: List[T]): Unit = {
    require(subList(l1, l2) && subList(l2, l1))
 
  }.ensuring(_ =>
    l1 == l2
  )
 
}