

Charles Babbage, looking ahead to the sorts of problems his Analytical Engine would be able to solve, gave this example:

 What is the smallest positive integer whose square ends in the digits 269,696?

— Babbage, letter to Lord Bowden, 1837; see Hollingdale and Tootill, Electronic Computers, second edition, 1970, p. 125.

He thought the answer might be 99,736, whose square is 9,947,269,696; but he couldn't be certain.



Task[edit]
The task is to find out if Babbage had the right answer — and to do so, as far as your language allows it, in code that Babbage himself would have been able to read and understand.
As Babbage evidently solved the task with pencil and paper, a similar efficient solution is preferred.

For these purposes, Charles Babbage may be taken to be an intelligent person, familiar with mathematics and with the idea of a computer; he has written the first drafts of simple computer programmes in tabular form. [Babbage Archive Series L].



Motivation
The aim of the task is to write a program that is sufficiently clear and well-documented for such a person to be able to read it and be confident that it does indeed solve the specified problem.




 
// Helper function for mask: does the actual computation.
function method mask_(v:int,m:int):int
  decreases v-m
  requires 0 <= v && 0 < m
  ensures v < mask_(v,m)
{
  if v < m then m else mask_(v,m*10)
}
 
// Return the smallest power of 10 greater than v.
function method mask(v:int):int
  requires 0 <= v
  ensures v < mask(v)
{
  mask_(v,10)
}
 
// Return true if the last digits of v == suffix.
predicate method EndWith(v:int,suffix:int)
  requires 0 <= suffix
{
  v % mask(suffix) == suffix
}
 
method SmallestSqEndingWith(suffix:int) returns (s:int)
  requires 0 < suffix
  ensures EndWith(s*s, suffix)
  // ensures forall i :: 0 <= i < s ==> !EndWith(i*i,suffix)
  decreases *                   // This method may not terminate.
{
  s := 0;
  // squares is the sequence of s*s. A ghost variable is only used by the
  // verification process at compile time.
  ghost var squares := [];
  while !EndWith(s*s, suffix)
    invariant s == |squares|
    invariant forall i :: 0 <= i < s ==> squares[i] == i*i && !EndWith(squares[i], suffix)
    decreases *
  {
    squares := squares + [s*s];
    s := s + 1;
  }
  // Leaving the method:
  // s*s ends with the suffix.
  assert EndWith(s*s, suffix);
  // The sequence squares contains i*i for i in [0..s]; none of the elements of
  // squares ends with the suffix.
  assert s == |squares|;
  assert forall i :: 0 <= i < s ==> i*i == squares[i] && !EndWith(squares[i], suffix);
  // That last assertion should imply the commented-out post-condition of the
  // method, but I'm not sure how to express that.
  //
  // Conclusion: s is guaranteed to be the smallest number whose square ends
  // with the suffix.
}
 
method Main() decreases *
{
  var suffix := 269696;
  var smallest := SmallestSqEndingWith(suffix);
  print smallest, "\n";
}
 