## Subsequence

Checking whether a word is a subsequence of another word.

**Auteurs:** Jean-Christophe Filliâtre

**Catégories:** Words / Algorithms

**Outils:** Why3

see also the index (by topic, by tool, by reference, by year)

# Subsequences

A subsequence is a sequence that can be derived from another sequence by deleting some or no elements without changing the order of the remaining elements (Wikipedia).

Checking whether a word is a subsequence of another word can be done in linear time (in the length of the second word) and is a nice example of an optimal greedy algorithm.

Author: Jean-Christophe FilliĆ¢tre (CNRS)

use int.Int use map.Map use seq.Seq type char type word = seq char predicate subsequence (v u: word) (f: int -> int) = (* f maps v's characters to u's characters *) (forall i. 0 <= i < length v -> 0 <= f i < length u /\ v[i] = u[f i]) /\ (* in a strictly increasing way *) (forall i j. 0 <= i < j < length v -> f i < f j) val eq (x y: char) : bool ensures { result <-> x = y } let is_subsequence (v u: word) : bool ensures { result <-> exists f. subsequence v u f } = let rec aux i j (ghost f) requires { 0 <= i <= length v } requires { 0 <= j <= length u } requires { subsequence v[0..i] u[0..j] f } requires { forall f. subsequence v u f -> i < length v -> f i >= j } variant { length u - j } ensures { result <-> exists f. subsequence v u f } = i = length v || j < length u && if eq v[i] u[j] then aux (i+1) (j+1) (Map.set f i j) else aux i (j+1) f in aux 0 0 (fun i -> i)

download ZIP archive

# Why3 Proof Results for Project "subsequence"

## Theory "subsequence.Top": fully verified

Obligations | CVC4 1.6 | CVC5 1.0.5 | ||||

VC for is_subsequence | --- | --- | ||||

split_vc | ||||||

variant decrease | 0.03 | --- | ||||

precondition | 0.04 | --- | ||||

precondition | 0.03 | --- | ||||

precondition | 0.28 | --- | ||||

precondition | 0.04 | --- | ||||

variant decrease | 0.03 | --- | ||||

precondition | 0.03 | --- | ||||

precondition | 0.04 | --- | ||||

precondition | 0.05 | --- | ||||

precondition | 0.02 | --- | ||||

postcondition | --- | --- | ||||

split_vc | ||||||

postcondition | --- | --- | ||||

split_vc | ||||||

postcondition | --- | --- | ||||

exists f | ||||||

is_subsequence'vc.10.0.0.0 | 0.06 | --- | ||||

postcondition | --- | 0.05 | ||||

postcondition | 0.04 | --- | ||||

precondition | 0.04 | --- | ||||

precondition | 0.04 | --- | ||||

precondition | 0.04 | --- | ||||

precondition | 0.04 | --- | ||||

postcondition | 0.02 | --- |