Articles

Verifying leftPad() in Whiley

The leftPad(string,int) function simply pads a string up to a given size by inserted spaces at the beginning. For example, leftPad("hello",8) produces " hello". This little function shot to fame in 2016 when a developer pulled all his modules from NPM, of which one provided the leftPad() functionality. There were two basic issues causing surprise here: firstly, a developer can suddenly and without warning pull all his libraries (including old versions), thereby breaking anything depending on them (which, in this case, was a lot). secondly, that someone was providing a module to offer this (pretty basic) functionality.

Anyhow, that is all ancient history. A bunch of people have been writing verified implementations of leftPad() in various languages. And, @Hillelolgram asked if I would write one in Whiley:

Twitter Thread

So, having little spare time, I thought I’d give it a crack. Here’s my first version:

import string from std::ascii
import char from std::ascii
import std::array

function leftPad(string str, int n) -> (string result)
// Required padding cannot be negative
requires n >= |str|
// Returned array increased to size n
ensures |result| == n
// First elements are padding
ensures all { i in 0 .. (n-|str|) | result[i] == ' '}
// Everything else copied from original
ensures all { i in 0 .. |str| | result[i+(n-|str|)] == str[i] }:
    // Calculate how much padding required
    int padding = n - |str|
    // Create new string of final length
    string nstr = [' '; n]
    // Copy over everthing from old string
    return array::copy(str,0,nstr,padding,|str|)

This is nice and short and makes use of the standard library. But, sadly, for reasons unknown I could not get this to pass verification. Since I already had a resize() method in the standard library and I knew this verified, I figured I could work from that instead. Here’s version two (after some faffing around):

function leftPad(string str, int size) -> (string result)
// Required padding cannot be negative
requires size >= |str|
// Returned array increased to size
ensures |result| == size
// First n elements are padding
ensures all { i in 0 .. (size-|str|) | result[i] == ' '}
// Everything else copied from original
ensures all { i in 0 .. |str| | result[i+(size-|str|)] == str[i] }:
    //
    int padding = size - |str|
    string nstr = [' '; size]
    int i = 0
    //
    while i < |str|
    where i >= 0 && |nstr| == size
    // All elements up to i copied over
    where all { j in 0..i | nstr[j+padding] == str[j] }
    // Untouched str are still padding
    where all { j in 0..padding | nstr[j] == ' ' }:
        //
        nstr[i+padding] = str[i]
        i = i + 1
    //
    return nstr

Essentially, I’ve inlined the call to array::copy(). And, yes, this verifies!! Unfortunately, you can’t verify it on whileylabs.com at the moment because it times out. But, you can do it using WhileyWeb or the command-line compiler.

Whilst it’s great that it does indeed verify, what’s less great is the faffing around I needed to get it through…

3 comments to Verifying leftPad() in Whiley

  • Arman Hatefi

    Dear Dr. Pearce,

    Very interesting post.

    Your first sample seems to be very straight forward. After a quick review I realized that the assignment at line 15 for Padding calculation should be written as n – |str|, because according to specification at line 07, n is greater than/equal to |str| and the current calculation in the post leads to negative values for Padding. Unfortunately, when I tried this new assignment in Whiley online compiler, it surprisingly gives me an “Internal failure: timeout” error message. So, I don’t know why the compiler cannot verify this change.

    I also checked out the implementation of array::copy method on GitHub and I think we need to add more specifications for arguments such as “srcStart”, “destStart” and “length” to be greater than/equal to Zero, because these arguments are used in the body of “copy” method to access and fetch the elements of the input arrays and they should always contain positive or Zero values.

    Thank you Dr. Pearce and hope we find the solutions soon.

  • Hey Arman,

    It won’t verify on whileylabs because of how long it takes to verify. The timeout is needed to to prevent the server collapsing under load. You can run it via the command-line tool, or by checking a local instance of WhileyWeb from here.

  • Hey Arman,

    You are also right about the array::copy method, though I haven’t tried to verify that. Which is presumably why it hasn’t been spotted!

    Otherwise, interesting comments!

Leave a Reply

 

 

 

You can use these HTML tags

<a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>