Object-Oriented Chapter 3 Summary

Prepare test data

This unit introduces the Junit unit test, which can construct data tests for each method by itself. However, because it needs to manually write the judgment premise and result constraint for each method, it is quite troublesome, so I will stop at Junit. Similar to the previous unit test, I still test this unit by randomly generating data.

The JML specification of the method constrains the premise and the result of the method, so the test for the method can be based on the JML bit to constrain the boundary conditions of the generated data to ensure that the data is legal and can cover all scopes. The JML constraints for data do not seem to be reflected in the JML specification of this unit, and the relevant constraints are all given in the instruction book. The invariants satisfied by the class can be satisfied on the premise of satisfying the constraints of each method, so there is no need to deliberately test. Therefore, the main purpose of constructing the data yourself is to test against the method.

When I wrote the code to generate data, considering the need to test the method, I gave each instruction a certain proportion: a balanced proportion can test the distribution of each instruction; deliberately increase the proportion of some instructions It can be tested to a certain extent. But random testing alone is not enough, because this unit runs on graphs, and in many cases, graphs of specific shapes need to be constructed for specific tests for specific instructions, so it is essential to construct data by yourself. For example, in the first assignment, you need to construct the worst case for the data of connected blocks, that is, each person belongs to an independent connected block, and then search and traverse repeatedly. If some students do not design well, they will time out. For another example, the second and third data for the spanning tree and the shortest path require additional construction, but because the number of these two types of instructions is limited, it will not timeout under normal circumstances.

Architecture design

Since this unit mainly trains the understanding of JML, the investigation of hierarchical design is relatively weak. Therefore, my implementation hierarchy in this unit is completely implemented according to the interface given by the official package, and the specific implementation is also completed according to the official JML.

Several algorithms worth mentioning, union search, minimum spanning tree and shortest path, are applied to three jobs respectively. Regarding the implementation of the union search set, I added path compression, because the official limit the number of instructions for the joiners, and the stack will not be blocked. For the minimum spanning tree and the shortest path, I used the heap-optimized versions of Prim and Dijkstra respectively, and the difference between the two implementations was only a few lines, so I implemented them in one method, distinguishing the two by passing in a type parameter.

The second is the selection of the container. Since it is necessary to find the lower-level object by id, I try to choose HashMap management, so that it can be completed with a very low time complexity when it is necessary to find the object corresponding to the id. Many students use ArrayList to manage objects according to the similar traversal method given by JML constraints, and traverse the container when searching, which increases the risk of being hack ed by timeout.

Network extension

/*@ public normal_behavior
  @ requires product != null;
  @ assignable customers;
  @ ensures (\forall int i; 0 <= i && i < customers.length; customers[i].contains(product));
  @ ensures (\forall int i; 0 <= i && i < customers.length;
  			\old(customers[i].contains(product)) ==> 
  			customers[i].product.length == \old(customers[i].product.length));
  @ ensures (\forall int i; 0 <= i && i < customers.length;
  			!\old(customers[i].contains(product)) ==> 
  			customers[i].product.length == \old(customers[i].product.length) + 1);
  @ ensures (\forall int i; 0 <= i && i < customers.length;
  			(\forall int j; 0 <= j && j < \old(customers[i].products.length); 
  			(\exists int z; 0 <= z && z < customers[i].products.length; customers[i].products[z] == \old(customers[i].products[j]))));
  public void advertiseForProducer(Product product);
  
/*@ public normal_behavior
  @ requires product != null;
  @ assignable producers;
  @ ensures (\forall int i; 0 <= i && i < producers.length; 
  			products[i] == product ==> producers[i].order[\old(producer[i].order.length)] == product);
  @ ensures (\forall int i; 0 <= i && i < producers.length;
  			(\forall int j; 0 <= j && j < \old(producers[i].order.length);
  			producers[i].order[j] == \old(producers[i].order[j])));
  public void buyForCustomer(Product product);
  
/*@ public normal_behavior
  @ requires product != null;
  @ assignable orders;
  @ ensures order[order.length] == product;
  @ ensures (\forall int i; 0 <= i && i < \old(order.length);
  			order[i] == \old(order[i]));
  public void newOrder(Product product);

learning experience

Specifications play an important role in software development. Using specifications not only facilitates the description of constraints on classes, methods, and data, but also disambiguates natural language expressions and facilitates cooperation between different developers. JML is a specific implementation of the specification. In this unit study, you can clearly feel that the syntax of JML is relatively simple, and the semantics that can be realized are rich, and it is easy to read after understanding the syntax.

The experience of specific operations is that it cannot be implemented completely according to the specification, but to focus on performance. A specification is just a constraint, as long as the effect achieved satisfies the constraint.