Longest common prefix

Verification challenge from VerifyThis: finding the least-common prefix of an array starting from two given indices.

General Information

Backend: Silicon
Language: PVL
Features: Arrays, Loop invariants, Quantified permissions
Path to Example File: verifythis/lcp.pvl
Should Verify: Yes
Date: 2017-06-21
Lines of Code: 25 (comments not included)
Lines of Specification: 13 (52.0% of total)

// -*- tab-width:2 ; indent-tabs-mode:nil -*-
//:: cases LeastCommonPrefix

class LCP {
	context_everywhere a != null;
	context_everywhere (\forall* int k; 0 <= k && k < a.length; Value(a[k]));
	context_everywhere 0 <= x && x < a.length;
	context_everywhere 0 <= y && y < a.length;
	ensures 0 <= \result + x && \result + x <= a.length;
	ensures 0 <= \result + y && \result + y <= a.length;
	ensures (\forall* int k; 0 <= k && k < a.length; Value(a[k]));
	ensures (\forall int k; 0 <= k && k < \result; a[x+k] == a[y+k]);
	int lcp(int[] a, int x, int y) {
	        int l = 0;

loop_invariant 0 <= l && l <= a.length; 
					loop_invariant 0 <= x+l && x+l <= a.length;
					loop_invariant 0 <= y+l && y+l <= a.length;
					loop_invariant (\forall* int k; 0 <= k && k < a.length; Value(a[k]));
					loop_invariant (\forall int k; 0 <= k && k < l; a[x+k] == a[y+k]); 
	        while (x+l < a.length && y+l < a.length && a[x+l] == a[y+l]) {
	          l = l + 1;
					}
					
	        return l;
	    }

}

Language: