Creating your project
Step 0: Create your project
You begin by writing your class in Java withprintf debugging. Make a directory where you would like to create your Java project and cd to that directory.
myapp/company/myapp.java, with the following content:
Using our SDK classes
Recall that the basic SDK workflow is:- Import the SDK classes that are being used.
- Use SDK classes in your code.
- Build your code, including the SDK as a build-time dependency.
- Deploy your build.
Step 1: Import the Java SDK assert class and jackson dependencies
For this example, the following jars are obtained from Maven Central, and stored in themyapp/lib directory:
Step 2. Use SDK classes in your code
You wrote a method to multiply numbers by ten. What sorts of properties should it have? The output should always be even. You should also make sure you are testing a wide variety of inputs, such as both even and odd numbers. Modify the code. The modifications are individually explained below.- Lines 3-6 You imported the Antithesis Java SDK and Jackson JSON support.
-
You added two assertions to times10.
- Line 22 You assert that the result is even using an Always Assertion. This is a fairly conventional assertion.
- Line 16 You insert a Sometimes Assertion, or an assertion that something will happen at least once across the entire testing session. You assert that sometimes during testing, the method will be called with an odd argument. The two types of assertions complement one another: Always Assertions assert that the behavior is correct, whereas Sometimes Assertions assert that you are testing under wide enough conditions to surface any potential incorrect behavior. In this case, the output would trivially be even if you only passed it even inputs — you must ensure your properties are not being trivially satisfied!
- Lines 29-32 You use randomness to call the method with many random values (between 0 and 500). Previously, you called the method with hardcoded values but now you will pass the function method values and test that the output is always even. This approach is more powerful but makes Sometimes Assertions necessary — now you must test that you are passing the method odd values, whereas previously the tests were hardcoded so you were certain that you were passing it odd values.
-
You call the method
getRandomto draw a random number, and then pass this random number totimes10. You use a loop to do this fifty times in a row. Every time the times10 method is called in this loop, it triggers the assertions in lines 16 & 22. -
In summary: You’ll test
times10by passing it a random integer fifty times in a row. You’ve asserted that all fifty outputs must be even and that at least one random input must be odd.
Preparing your project for Antithesis
To send code to Antithesis, you should build as described above. Antithesis will explore your software and search for violations of the properties you have defined. You must send us containers as described in getting started. The executable jar should be included in your container. In this example, the jar would containcompany/myapp.class.
This example is simplified compared to what the full quickstart guide describes. Note
that the method
main is the workload and times10 is the software itself.
There are no dependencies.