McCarthy 91 function, Java version
McCarthy 91 function
Authors: Claude Marché
Topics: Tricky termination / Historical examples
Tools: Krakatoa
see also the index (by topic, by tool, by reference, by year)
/**************************************************************************/ /* */ /* The Why platform for program certification */ /* */ /* Copyright (C) 2002-2011 */ /* */ /* Jean-Christophe FILLIATRE, CNRS & Univ. Paris-sud 11 */ /* Claude MARCHE, INRIA & Univ. Paris-sud 11 */ /* Yannick MOY, Univ. Paris-sud 11 */ /* Romain BARDOU, Univ. Paris-sud 11 */ /* */ /* Secondary contributors: */ /* */ /* Thierry HUBERT, Univ. Paris-sud 11 (former Caduceus front-end) */ /* Nicolas ROUSSET, Univ. Paris-sud 11 (on Jessie & Krakatoa) */ /* Ali AYAD, CNRS & CEA Saclay (floating-point support) */ /* Sylvie BOLDO, INRIA (floating-point support) */ /* Jean-Francois COUCHOT, INRIA (sort encodings, hyps pruning) */ /* Mehdi DOGGUY, Univ. Paris-sud 11 (Why GUI) */ /* */ /* This software is free software; you can redistribute it and/or */ /* modify it under the terms of the GNU Lesser General Public */ /* License version 2.1, with the special exception on linking */ /* described in file LICENSE. */ /* */ /* This software is distributed in the hope that it will be useful, */ /* but WITHOUT ANY WARRANTY; without even the implied warranty of */ /* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. */ /* */ /**************************************************************************/ /* McCarthy's ``91'' function. */ public class MacCarthy { /*@ decreases 101-n ; @ behavior less_than_101: @ assumes n <= 100; @ ensures \result == 91; @ behavior greater_than_100: @ assumes n >= 101; @ ensures \result == n - 10; @*/ public static int f91(int n) { if (n <= 100) { return f91(f91(n + 11)); } else return n - 10; } } /* Local Variables: compile-command: "make MacCarthy.why3ml" End: */