1/* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 6 * See "LICENSE_BSD2.txt" for details. 7 * 8 * @TAG(NICTA_BSD) 9 */ 10 11unsigned int fact(unsigned int n) 12{ 13 unsigned int total, factor; 14 total = 1; 15 factor = 2; 16 while (factor <= n) 17 /** INV: "\<lbrace>\<acute>factor * \<acute>total = FACT \<acute>factor & \<acute>factor <= max 2 (\<acute>n + 1) \<rbrace>" */ 18 { 19 total = total * factor; 20 factor = factor + 1; 21 } 22 return total; 23} 24