Verify small Java program using OpenJML tool

Prove partial correctness of the program Fact.java (that is, without proof of finality) using OpenJML.
You should:
* Write preconditions (if necessary), and postconditions (required)
* Write a loop invariant