Skip to content

Commit 6b72669

Browse files
bzp99bzp99
committed
Fix JML specs
1 parent e6b62b7 commit 6b72669

File tree

23 files changed

+144
-41
lines changed

23 files changed

+144
-41
lines changed

‎smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/TPCC.jml renamed to ‎smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/api/TPCCBusinessAPI.jml

Lines changed: 25 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,23 @@
11
/* SPDX-License-Identifier: Apache-2.0 */
2+
package hu.bme.mit.ftsrg.chaincode.tpcc.api;
23

3-
package hu.bme.mit.ftsrg.chaincode.tpcc;
4-
5-
import hu.bme.mit.ftsrg.hypernate.entity.EntityExistsException;
6-
import hu.bme.mit.ftsrg.hypernate.entity.EntityNotFoundException;
4+
import com.fasterxml.jackson.core.JsonProcessingException;
5+
import com.jcabi.aspects.Loggable;
6+
import hu.bme.mit.ftsrg.chaincode.tpcc.data.entity.*;
7+
import hu.bme.mit.ftsrg.chaincode.tpcc.data.extra.*;
78
import hu.bme.mit.ftsrg.chaincode.tpcc.data.input.*;
89
import hu.bme.mit.ftsrg.chaincode.tpcc.data.output.*;
910
import hu.bme.mit.ftsrg.chaincode.tpcc.middleware.TPCCContext;
10-
import org.hyperledger.fabric.contract.ContractInterface;
11+
import hu.bme.mit.ftsrg.hypernate.Registry;
12+
import hu.bme.mit.ftsrg.hypernate.context.ContextWithRegistry;
13+
import hu.bme.mit.ftsrg.hypernate.entity.EntityExistsException;
14+
import hu.bme.mit.ftsrg.hypernate.entity.EntityNotFoundException;
15+
import hu.bme.mit.ftsrg.hypernate.entity.SerializationException;
16+
import java.util.*;
17+
import org.slf4j.Logger;
1118

12-
public final class TPCC implements ContractInterface {
19+
@Loggable(Loggable.DEBUG)
20+
class TPCCBusinessAPI {
1321

1422
/*@
1523
@ ensures \result.getW_id() == input.getW_id(); // C.TXIO:DELIVERY:EQ_W_ID
@@ -18,8 +26,8 @@ public final class TPCC implements ContractInterface {
1826
@ ensures \result.getSkipped() >= 0 & \result.getSkipped() <= 10; // C.TXIO:DELIVERY:LIM_SKIPPED
1927
@ ensures \result.getSkipped() == 10 - \result.getDelivered().size(); // C.TXIO:DELIVERY:FORM_SKIPPED
2028
@*/
21-
private DeliveryOutput delivery(final TPCCContext ctx, final DeliveryInput input)
22-
throws EntityNotFoundException;
29+
DeliveryOutput delivery(final TPCCContext ctx, final DeliveryInput input)
30+
throws EntityNotFoundException, SerializationException, JsonProcessingException;
2331

2432
/*@
2533
@ ensures \result.getW_id() == input.getW_id(); // C.TXIO:NEWORDER:EQ_W_ID
@@ -28,16 +36,16 @@ public final class TPCC implements ContractInterface {
2836
@ ensures \result.getO_ol_cnt() == input.getI_ids().length; // C.TXIO:NEWORDER:SIZE_OL_CNT
2937
@ ensures \result.getItems().size() == input.getI_ids().length; // C.TXIO:NEWORDER:SIZE_ITEMS
3038
@*/
31-
private NewOrderOutput newOrder(final TPCCContext ctx, final NewOrderInput input)
32-
throws EntityNotFoundException, EntityExistsException;
39+
NewOrderOutput newOrder(final TPCCContext ctx, final NewOrderInput input)
40+
throws EntityNotFoundException, EntityExistsException, SerializationException;
3341

3442
/*@
3543
@ ensures \result.getW_id() == input.getW_id(); // C.TXIO:ORDERSTATUS:EQ_W_ID
3644
@ ensures \result.getD_id() == input.getD_id(); // C.TXIO:ORDERSTATUS:EQ_D_ID
3745
@ ensures \result.getC_id() == input.getC_id(); // C.TXIO:ORDERSTATUS:EQ_D_ID
3846
@*/
39-
private OrderStatusOutput orderStatus(final TPCCContext ctx, final OrderStatusInput input)
40-
throws NotFoundException, EntityNotFoundException;
47+
OrderStatusOutput orderStatus(final TPCCContext ctx, final OrderStatusInput input)
48+
throws NotFoundException, EntityNotFoundException, SerializationException, JsonProcessingException;
4149

4250
/*@
4351
@ ensures \result.getW_id() == input.getW_id(); // C.TXIO:PAYMENT:EQ_W_ID
@@ -46,20 +54,17 @@ public final class TPCC implements ContractInterface {
4654
@ ensures \result.getH_amount() == input.getH_amount(); // C.TXIO:PAYMENT:EQ_H_AMOUNT
4755
@ ensures \result.getH_date() == input.getH_date(); // C.TXIO:PAYMENT:EQ_H_DATE
4856
@*/
49-
private PaymentOutput payment(final TPCCContext ctx, final PaymentInput input)
50-
throws EntityNotFoundException, EntityExistsException, NotFoundException;
57+
PaymentOutput payment(final TPCCContext ctx, final PaymentInput input)
58+
throws EntityNotFoundException, EntityExistsException, NotFoundException, SerializationException, JsonProcessingException;
5159

5260
/*@
5361
@ ensures \result.getW_id() == input.getW_id(); // C.TXIO:STOCKLEVEL:EQ_W_ID
5462
@ ensures \result.getD_id() == input.getD_id(); // C.TXIO:STOCKLEVEL:EQ_D_ID
5563
@ ensures \result.getThreshold() == input.getThreshold(); // C.TXIO:STOCKLEVEL:EQ_THRESHOLD
5664
@ ensures \result.getLow_stock() >= 0; // C.TXIO:STOCKLEVEL:LIM_LOW_STOCK
5765
@*/
58-
private StockLevelOutput stockLevel(final TPCCContext ctx, final StockLevelInput input)
59-
throws EntityNotFoundException, NotFoundException;
66+
StockLevelOutput stockLevel(final TPCCContext ctx, final StockLevelInput input)
67+
throws EntityNotFoundException, NotFoundException, SerializationException;
6068

61-
/*@
62-
@ requires c_id < 2;
63-
@*/
64-
public String OJMLTEST__getCustomer(final TPCCContext ctx, final int c_w_id, final int c_d_id, final int c_id);
69+
void init(final TPCCContext ctx) throws EntityExistsException;
6570
}

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

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
/* SPDX-License-Identifier: Apache-2.0 */
2+
package hu.bme.mit.ftsrg.chaincode.tpcc.api;
3+
4+
import com.fasterxml.jackson.core.JsonProcessingException;
5+
import com.jcabi.aspects.Loggable;
6+
import hu.bme.mit.ftsrg.chaincode.tpcc.middleware.TPCCContext;
7+
import org.hyperledger.fabric.contract.ContractInterface;
8+
import org.hyperledger.fabric.contract.annotation.Contact;
9+
import org.hyperledger.fabric.contract.annotation.Contract;
10+
import org.hyperledger.fabric.contract.annotation.Default;
11+
import org.hyperledger.fabric.contract.annotation.Info;
12+
import org.hyperledger.fabric.contract.annotation.License;
13+
import org.hyperledger.fabric.contract.annotation.Transaction;
14+
15+
@Contract(
16+
name = "TPCC",
17+
info =
18+
@Info(
19+
title = "tpcc contract",
20+
description = "My Smart Contract",
21+
version = "0.0.1",
22+
license = @License(name = "Apache-2.0"),
23+
contact =
24+
@Contact(email = "[email protected]", name = "tpcc", url = "http://tpcc.me")))
25+
26+
@Default
27+
@Loggable(Loggable.DEBUG)
28+
public final class TPCCContractAPI implements ContractInterface {
29+
30+
/*@
31+
@ requires c_id < 2;
32+
@*/
33+
@Transaction(intent = Transaction.TYPE.EVALUATE)
34+
public String OJMLTEST__getCustomer(final TPCCContext ctx, final int c_w_id, final int c_d_id, final int c_id) throws JsonProcessingException;
35+
}

‎smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/entity/Customer.jml

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,12 @@
11
/* SPDX-License-Identifier: Apache-2.0 */
2-
32
package hu.bme.mit.ftsrg.chaincode.tpcc.data.entity;
43

54
import hu.bme.mit.ftsrg.hypernate.entity.Entity;
5+
import lombok.EqualsAndHashCode;
6+
import org.hyperledger.fabric.contract.annotation.DataType;
67

8+
@EqualsAndHashCode
9+
@DataType
710
public final class Customer implements Entity {
811

912
public /*@ pure @*/ int getC_id();

‎smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/entity/District.jml

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,12 @@
11
/* SPDX-License-Identifier: Apache-2.0 */
2-
32
package hu.bme.mit.ftsrg.chaincode.tpcc.data.entity;
43

54
import hu.bme.mit.ftsrg.hypernate.entity.Entity;
5+
import lombok.EqualsAndHashCode;
6+
import org.hyperledger.fabric.contract.annotation.DataType;
67

8+
@EqualsAndHashCode
9+
@DataType
710
public final class District implements Entity {
811

912
public /*@ pure @*/ int getD_id();

‎smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/entity/History.jml

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,12 @@
11
/* SPDX-License-Identifier: Apache-2.0 */
2-
32
package hu.bme.mit.ftsrg.chaincode.tpcc.data.entity;
43

54
import hu.bme.mit.ftsrg.hypernate.entity.Entity;
5+
import lombok.EqualsAndHashCode;
6+
import org.hyperledger.fabric.contract.annotation.DataType;
67

8+
@EqualsAndHashCode
9+
@DataType
710
public final class History implements Entity {
811

912
public /*@ pure @*/ int getH_c_id();

‎smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/entity/Item.jml

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,12 @@
11
/* SPDX-License-Identifier: Apache-2.0 */
2-
32
package hu.bme.mit.ftsrg.chaincode.tpcc.data.entity;
43

54
import hu.bme.mit.ftsrg.hypernate.entity.Entity;
5+
import lombok.EqualsAndHashCode;
6+
import org.hyperledger.fabric.contract.annotation.DataType;
67

8+
@EqualsAndHashCode
9+
@DataType
710
public final class Item implements Entity {
811

912
public /*@ pure @*/ int getI_id();

‎smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/entity/NewOrder.jml

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,12 @@
11
/* SPDX-License-Identifier: Apache-2.0 */
2-
32
package hu.bme.mit.ftsrg.chaincode.tpcc.data.entity;
43

54
import hu.bme.mit.ftsrg.hypernate.entity.Entity;
5+
import lombok.EqualsAndHashCode;
6+
import org.hyperledger.fabric.contract.annotation.DataType;
67

8+
@EqualsAndHashCode
9+
@DataType
710
public final class NewOrder implements Entity {
811

912
public /*@ pure @*/ int getNo_o_id();

‎smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/entity/Order.jml

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,12 @@
11
/* SPDX-License-Identifier: Apache-2.0 */
2-
32
package hu.bme.mit.ftsrg.chaincode.tpcc.data.entity;
43

54
import hu.bme.mit.ftsrg.hypernate.entity.Entity;
5+
import lombok.EqualsAndHashCode;
6+
import org.hyperledger.fabric.contract.annotation.DataType;
67

8+
@EqualsAndHashCode
9+
@DataType
710
public final class Order implements Entity {
811

912
public /*@ pure @*/ int getO_id();

‎smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/entity/OrderLine.jml

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,12 @@
11
/* SPDX-License-Identifier: Apache-2.0 */
2-
32
package hu.bme.mit.ftsrg.chaincode.tpcc.data.entity;
43

54
import hu.bme.mit.ftsrg.hypernate.entity.Entity;
5+
import lombok.EqualsAndHashCode;
6+
import org.hyperledger.fabric.contract.annotation.DataType;
67

8+
@EqualsAndHashCode
9+
@DataType
710
public final class OrderLine implements Entity {
811

912
public /*@ pure @*/ int getOl_o_id();

‎smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/entity/Stock.jml

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,12 @@
11
/* SPDX-License-Identifier: Apache-2.0 */
2-
32
package hu.bme.mit.ftsrg.chaincode.tpcc.data.entity;
43

54
import hu.bme.mit.ftsrg.hypernate.entity.Entity;
5+
import lombok.EqualsAndHashCode;
6+
import org.hyperledger.fabric.contract.annotation.DataType;
67

8+
@EqualsAndHashCode
9+
@DataType
710
public final class Stock implements Entity {
811

912
public /*@ pure @*/ int getS_i_id();

‎smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/entity/Warehouse.jml

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,12 @@
11
/* SPDX-License-Identifier: Apache-2.0 */
2-
32
package hu.bme.mit.ftsrg.chaincode.tpcc.data.entity;
43

54
import hu.bme.mit.ftsrg.hypernate.entity.Entity;
5+
import lombok.EqualsAndHashCode;
6+
import org.hyperledger.fabric.contract.annotation.DataType;
67

8+
@EqualsAndHashCode
9+
@DataType
710
public class Warehouse implements Entity {
811

912
public /*@ pure @*/ int getW_id();

‎smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/input/DeliveryInput.jml

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,11 @@
11
/* SPDX-License-Identifier: Apache-2.0 */
2-
32
package hu.bme.mit.ftsrg.chaincode.tpcc.data.input;
43

4+
import lombok.EqualsAndHashCode;
5+
import org.hyperledger.fabric.contract.annotation.DataType;
6+
7+
@EqualsAndHashCode
8+
@DataType
59
public final class DeliveryInput {
610

711
public /*@ pure @*/ int getW_id();

‎smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/input/NewOrderInput.jml

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,11 @@
11
/* SPDX-License-Identifier: Apache-2.0 */
2-
32
package hu.bme.mit.ftsrg.chaincode.tpcc.data.input;
43

4+
import lombok.EqualsAndHashCode;
5+
import org.hyperledger.fabric.contract.annotation.DataType;
6+
7+
@EqualsAndHashCode
8+
@DataType
59
public final class NewOrderInput {
610

711
public /*@ pure @*/ int getW_id();

‎smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/input/OrderStatusInput.jml

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,11 @@
11
/* SPDX-License-Identifier: Apache-2.0 */
2-
32
package hu.bme.mit.ftsrg.chaincode.tpcc.data.input;
43

4+
import lombok.EqualsAndHashCode;
5+
import org.hyperledger.fabric.contract.annotation.DataType;
6+
7+
@EqualsAndHashCode
8+
@DataType
59
public final class OrderStatusInput {
610

711
public /*@ pure @*/ int getW_id();

‎smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/input/PaymentInput.jml

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,11 @@
11
/* SPDX-License-Identifier: Apache-2.0 */
2-
32
package hu.bme.mit.ftsrg.chaincode.tpcc.data.input;
43

4+
import lombok.EqualsAndHashCode;
5+
import org.hyperledger.fabric.contract.annotation.DataType;
6+
7+
@EqualsAndHashCode
8+
@DataType
59
public final class PaymentInput {
610

711
public /*@ pure @*/ int getW_id();

‎smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/input/StockLevelInput.jml

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,11 @@
11
/* SPDX-License-Identifier: Apache-2.0 */
2-
32
package hu.bme.mit.ftsrg.chaincode.tpcc.data.input;
43

4+
import lombok.EqualsAndHashCode;
5+
import org.hyperledger.fabric.contract.annotation.DataType;
6+
7+
@EqualsAndHashCode
8+
@DataType
59
public final class StockLevelInput {
610

711
public /*@ pure @*/ int getW_id();

‎smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/output/DeliveryOutput.jml

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,13 @@
11
/* SPDX-License-Identifier: Apache-2.0 */
2-
32
package hu.bme.mit.ftsrg.chaincode.tpcc.data.output;
43

54
import hu.bme.mit.ftsrg.chaincode.tpcc.data.extra.DeliveredOrder;
65
import java.util.List;
6+
import lombok.EqualsAndHashCode;
7+
import org.hyperledger.fabric.contract.annotation.DataType;
78

9+
@EqualsAndHashCode
10+
@DataType
811
public final class DeliveryOutput {
912

1013
public /*@ pure @*/ int getW_id();

‎smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/output/NewOrderOutput.jml

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,13 @@
11
/* SPDX-License-Identifier: Apache-2.0 */
2-
32
package hu.bme.mit.ftsrg.chaincode.tpcc.data.output;
43

54
import hu.bme.mit.ftsrg.chaincode.tpcc.data.extra.ItemsData;
65
import java.util.List;
6+
import lombok.EqualsAndHashCode;
7+
import org.hyperledger.fabric.contract.annotation.DataType;
78

9+
@EqualsAndHashCode
10+
@DataType
811
public final class NewOrderOutput {
912

1013
public /*@ pure @*/ int getW_id();

‎smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/output/OrderStatusOutput.jml

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,12 @@
11
/* SPDX-License-Identifier: Apache-2.0 */
2-
32
package hu.bme.mit.ftsrg.chaincode.tpcc.data.output;
43

54
import java.util.List;
5+
import lombok.EqualsAndHashCode;
6+
import org.hyperledger.fabric.contract.annotation.DataType;
67

8+
@EqualsAndHashCode
9+
@DataType
710
public final class OrderStatusOutput {
811

912
public /*@ pure @*/ int getW_id();

‎smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/output/PaymentOutput.jml

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,11 @@
11
/* SPDX-License-Identifier: Apache-2.0 */
2-
32
package hu.bme.mit.ftsrg.chaincode.tpcc.data.output;
43

4+
import lombok.EqualsAndHashCode;
5+
import org.hyperledger.fabric.contract.annotation.DataType;
6+
7+
@EqualsAndHashCode
8+
@DataType
59
public final class PaymentOutput {
610

711
public /*@ pure @*/ int getW_id();

‎smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/output/StockLevelOutput.jml

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,11 @@
11
/* SPDX-License-Identifier: Apache-2.0 */
2-
32
package hu.bme.mit.ftsrg.chaincode.tpcc.data.output;
43

4+
import lombok.EqualsAndHashCode;
5+
import org.hyperledger.fabric.contract.annotation.DataType;
6+
7+
@EqualsAndHashCode
8+
@DataType
59
public final class StockLevelOutput {
610

711
public /*@ pure @*/ int getW_id();

‎smart-contract/hyperledger-fabric/v2/java/src/main/java/hu/bme/mit/ftsrg/chaincode/tpcc/data/entity/Customer.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@
99

1010
/** Essentially, the CUSTOMER table. */
1111
@EqualsAndHashCode
12-
@DataType()
12+
@DataType
1313
public final class Customer implements Entity {
1414

1515
/** The customer ID. Primary key. */

0 commit comments

Comments
 (0)