In this first lab, you will use Stainless to verify programs.

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

To verify your code, run stainless –timeout=10 SubList.scala (you can also add –watch if you want to actively edit your file).

Additionally, if you want to compile and execute your code (you don't have to), run (with Scala 2.12.9 and with /path/to/stainless pointing to the Stainless repository from GitHub checked out on your machine):

scalac $(find /path/to/stainless/frontends/library/stainless/ -name "*.scala") SubList.scala
scala SubList

Upload your solutions on Moodle by Friday 25th 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

Some advice:

• try to understand how you would prove these properties with paper and pencil, and use examples of lists to gain intuition
• induction is one of the main methods needed in many cases, see the videos on how to write inductive proofs
• even though simplest cases may work automatically, in general you may need to prove additional lemmas
• prove lemmas in order; earlier lemmas (and their structure) will help you with subsequent lemmas

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
  )
 
  @extern
  def main(args: Array[String]): Unit = {
    println(subList(List(0, 2), List(0, 1, 2))) // true
    println(subList(List(1, 0), List(0, 0, 1))) // false
    println(subList(List(10, 5, 25), List(70, 10, 11, 8, 5, 25, 22))) // true
  }
 
}