Verifying string reverse with Dafny (https://github.com/Microsoft/dafny)

reverse.dfy

# See https://tio.run/##dU9BboNADDzDK6Y3UEobegQ2L@ipV8TBEkuxcBZ1gVRRk7fT3aVVVTW9WOOxPZ5pqTPndT3quR9bvOiTtpNOqABZS@eKzXxI48jqt4WtnkC4UzCLSBlHx7Hljj3pGm2mxS90oyURDCgK7FEphyrQw7M2r3MPpQ6gemgcwChtQnXyPcvyFBmGJi3jjzg6kYWgUD@nGfJy49nze9e89ywaCbsPkrGzGbFxC0xm3n6zL4ns8vTxqfw1vmmTcbl4JQcHz8kNv5IFi/9p8ZeWCjp/z7djFzCimpt7eEFuQtCAPMNN0PckYxdiX@Prun4C
method Reverse(a: array<int>)
	requires a != null;
	modifies a;
	ensures forall k :: 0 <= k < a.Length ==> a[k] == old(a[(a.Length-1) - k]);
{
	var l := a.Length - 1;
	var i := 0;
	while (i < l-i)
		invariant 0 <= i <= (l+1)/2;
		invariant forall k :: 0 <= k < i || l-i < k <= l ==> a[k] == old(a[l-k]);
		invariant forall k :: i <= k <= l-i ==> a[k] == old(a[k]);
	{
		a[i], a[l-i] := a[l-i], a[i];
		i := i + 1;
	}
}