Move OJMLTEST__getCustomer JML specs to JML file

Apparently, if a JML spec file exists, OpenJML ignores specs defined in
the Java source file.  In other words, any existing JML file supersedes
Java files in terms of JML specs.

Author: bzp99

smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/TPCC.jml

@@ -57,4 +57,9 @@ public final class TPCC implements ContractInterface {
     @*/
   private StockLevelOutput stockLevel(final TPCCContext ctx, final StockLevelInput input)
       throws EntityNotFoundException, NotFoundException;
+
+  /*@
+    @ requires c_id < 2;
+    @*/
+  public String OJMLTEST__getCustomer(final TPCCContext ctx, final int c_w_id, final int c_d_id, final int c_id);
 }

smart-contract/hyperledger-fabric/v2/java/src/main/java/hu/bme/mit/ftsrg/chaincode/tpcc/TPCC.java

@@ -305,9 +305,6 @@ public String ping(final TPCCContext ctx) {
    * @return The customer with matching (C_W_ID, C_D_ID, C_ID), unless C_ID >= 2, in which case an
    *     exception should be thrown by OpenJML
    */
-  // spotless:off
-  //@ requires c_id < 2;
-  // spotless:on
   @Transaction(intent = Transaction.TYPE.EVALUATE)
   public String OJMLTEST__getCustomer(
       final TPCCContext ctx, final int c_w_id, final int c_d_id, final int c_id) {