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:

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…
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!
XVII century was Nicholas Jarry [fr].
XVII century was Nicholas Jarry [fr].
55 thousand Greek, 30 thousand Armenian
“Julia’s Garland” (fr. Guirlande de Julie)
bride, Julie d’Angenne.
from lat. manus – “hand” and scribo – “I write”) [1]
XVII century was Nicholas Jarry [fr].
Western Europe also formed