Uses Dafny Syntax

Fill in the annotations at the designated places. You can use the function (Factorial) in the annotations. Fill in the two loop invariants and the assertion. function Factorial (n: int): int requires n- 0 if n0 then 1 else n * Factorial (n-1) method LoopyFactorial (n: int) returns (u: int) requires n0 ensures uFactorial (n) var r :-0; while (r