|
8 | 8 | import io.modelcontextprotocol.client.transport.StdioClientTransport; |
9 | 9 | import io.modelcontextprotocol.json.McpJsonDefaults; |
10 | 10 | import io.modelcontextprotocol.spec.McpSchema.CallToolRequest; |
| 11 | +import io.modelcontextprotocol.spec.McpSchema.CallToolResult; |
11 | 12 | import java.nio.file.Path; |
12 | 13 | import java.time.Duration; |
13 | 14 | import java.util.List; |
@@ -37,166 +38,89 @@ void stopServer() { |
37 | 38 | } |
38 | 39 |
|
39 | 40 | @Test |
40 | | - void advertisesVerifyAndReturnsStructuredOutput() throws Exception { |
| 41 | + void advertisesTools() { |
41 | 42 | var tools = client.listTools().tools(); |
42 | 43 | assertEquals(List.of("verify", "get_diagnostics", "get_locals", "get_globals", "get_contracts", "check_validity", "check_satisfiability", "get_state_machine"), tools.stream().map(tool -> tool.name()).toList()); |
43 | | - |
44 | | - var result = client.callTool(verifyRequest("Valid.java")); |
45 | | - assertFalse(result.isError()); |
46 | | - var content = (Map<?, ?>) result.structuredContent(); |
47 | | - assertEquals(true, content.get("success")); |
48 | | - assertTrue(((String) content.get("output")).contains("Correct! Passed Verification.")); |
49 | | - assertTrue(McpJsonDefaults.getSchemaValidator().validate(tools.getFirst().outputSchema(), content).valid()); |
50 | 44 | } |
51 | 45 |
|
52 | 46 | @Test |
53 | | - void returnsDebugOutputOverStdioWithoutLeakingIntoTheNextCall() throws Exception { |
54 | | - var path = verifyRequest("Invalid.java").arguments().get("path"); |
55 | | - var result = client.callTool(new CallToolRequest("verify", Map.of("path", path, "debug", true))); |
56 | | - assertFalse(result.isError()); |
57 | | - var content = (Map<?, ?>) result.structuredContent(); |
58 | | - assertEquals(false, content.get("success")); |
59 | | - assertTrue(((String) content.get("output")).contains("[SMT]")); |
60 | | - assertTrue(((String) content.get("output")).contains("Refinement Error")); |
61 | | - |
62 | | - var quiet = client.callTool(verifyRequest("Valid.java")); |
63 | | - assertFalse(quiet.isError()); |
64 | | - var quietContent = (Map<?, ?>) quiet.structuredContent(); |
65 | | - assertEquals(true, quietContent.get("success")); |
66 | | - assertFalse(((String) quietContent.get("output")).contains("[SMT]")); |
| 47 | + void verifyTool() { |
| 48 | + CallToolRequest request = CallToolRequest.builder("verify").arguments( |
| 49 | + Map.of("path", examplePath("Valid.java")) |
| 50 | + ).build(); |
| 51 | + CallToolResult result = client.callTool(request); |
| 52 | + assertFalse(result.isError(), result.toString()); |
67 | 53 | } |
68 | 54 |
|
69 | 55 | @Test |
70 | | - void reportsRefinementFailureAsANormalToolResult() { |
71 | | - var result = client.callTool(verifyRequest("Invalid.java")); |
72 | | - assertFalse(result.isError()); |
73 | | - var content = (Map<?, ?>) result.structuredContent(); |
74 | | - assertEquals(false, content.get("success")); |
75 | | - assertTrue(((String) content.get("output")).contains("Refinement Error")); |
| 56 | + void getDiagnosticsTool() { |
| 57 | + CallToolRequest request = CallToolRequest.builder("get_diagnostics").arguments( |
| 58 | + Map.of("path", examplePath("Counterexample.java")) |
| 59 | + ).build(); |
| 60 | + CallToolResult result = client.callTool(request); |
| 61 | + assertFalse(result.isError(), result.toString()); |
76 | 62 | } |
77 | 63 |
|
78 | 64 | @Test |
79 | | - void invalidInputUsesTheStructuredErrorContract() { |
80 | | - var result = client.callTool(new CallToolRequest("verify", Map.of())); |
81 | | - assertTrue(result.isError()); |
82 | | - var content = (Map<?, ?>) result.structuredContent(); |
83 | | - assertEquals(false, content.get("success")); |
84 | | - assertEquals("INVALID_INPUT", ((Map<?, ?>) content.get("error")).get("code")); |
| 65 | + void getLocalsTool() { |
| 66 | + CallToolRequest request = CallToolRequest.builder("get_locals").arguments( |
| 67 | + Map.of("path", examplePath("Context.java"), "line", 12, "column", 9) |
| 68 | + ).build(); |
| 69 | + CallToolResult result = client.callTool(request); |
| 70 | + assertFalse(result.isError(), result.toString()); |
85 | 71 | } |
86 | 72 |
|
87 | 73 | @Test |
88 | | - void returnsDiagnosticsOverStdio() throws Exception { |
89 | | - var tool = client.listTools().tools().stream() |
90 | | - .filter(candidate -> candidate.name().equals("get_diagnostics")).findFirst().orElseThrow(); |
91 | | - var result = client.callTool(new CallToolRequest("get_diagnostics", verifyRequest("Counterexample.java").arguments())); |
92 | | - assertFalse(result.isError()); |
93 | | - var content = (Map<?, ?>) result.structuredContent(); |
94 | | - assertEquals(false, content.get("success")); |
95 | | - var diagnostic = (Map<?, ?>) ((List<?>) content.get("errors")).getFirst(); |
96 | | - assertEquals("RefinementError", diagnostic.get("type")); |
97 | | - assertNotNull(diagnostic.get("counterexample")); |
98 | | - assertTrue(McpJsonDefaults.getSchemaValidator().validate(tool.outputSchema(), content).valid()); |
99 | | - var invalid = client.callTool(new CallToolRequest("get_diagnostics", Map.of())); |
100 | | - assertTrue(invalid.isError()); |
101 | | - assertTrue(McpJsonDefaults.getSchemaValidator().validate(tool.outputSchema(), invalid.structuredContent()).valid()); |
| 74 | + void getGlobalsTool() { |
| 75 | + CallToolRequest request = CallToolRequest.builder("get_globals").arguments( |
| 76 | + Map.of("path", examplePath("Context.java")) |
| 77 | + ).build(); |
| 78 | + CallToolResult result = client.callTool(request); |
| 79 | + assertFalse(result.isError(), result.toString()); |
102 | 80 | } |
103 | 81 |
|
104 | 82 | @Test |
105 | | - void returnsContextOverStdio() throws Exception { |
106 | | - String file = Path.of("src/test/resources/examples/Context.java").toAbsolutePath().toString(); |
107 | | - for (String name : List.of("get_locals", "get_globals")) { |
108 | | - var tool = client.listTools().tools().stream() |
109 | | - .filter(t -> t.name().equals(name)).findFirst().orElseThrow(); |
110 | | - var arguments = name.equals("get_locals") |
111 | | - ? Map.<String, Object>of("path", file, "file", file, "line", 12, "column", 9) |
112 | | - : Map.<String, Object>of("path", file, "file", file); |
113 | | - var result = client.callTool(new CallToolRequest(name, arguments)); |
114 | | - assertFalse(result.isError(), result.toString()); |
115 | | - var content = (Map<?, ?>) result.structuredContent(); |
116 | | - assertFalse(content.containsKey("errors")); |
117 | | - assertFalse(content.containsKey("warnings")); |
118 | | - assertTrue(McpJsonDefaults.getSchemaValidator().validate(tool.outputSchema(), content).valid()); |
119 | | - if (name.equals("get_locals")) { |
120 | | - var variables = (List<Map<String, Object>>) content.get("variables"); |
121 | | - assertTrue(variables.stream().anyMatch(v -> v.get("name").equals("input"))); |
122 | | - assertTrue(variables.stream().anyMatch(v -> v.get("name").equals("first"))); |
123 | | - assertFalse(variables.stream().anyMatch(v -> List.of("nested", "last", "unrelated").contains(v.get("name")))); |
124 | | - } else { |
125 | | - assertTrue(((List<Map<String, Object>>) content.get("aliases")).stream().anyMatch(a -> a.get("name").equals("Positive"))); |
126 | | - assertTrue(((List<Map<String, Object>>) content.get("ghosts")).stream().anyMatch(g -> g.get("name").equals("size"))); |
127 | | - assertEquals(2, ((List<?>) content.get("states")).size()); |
128 | | - } |
129 | | - var invalid = client.callTool(new CallToolRequest(name, Map.of())); |
130 | | - assertTrue(invalid.isError()); |
131 | | - assertTrue(McpJsonDefaults.getSchemaValidator().validate(tool.outputSchema(), invalid.structuredContent()).valid()); |
132 | | - } |
| 83 | + void getContractsTool() { |
| 84 | + CallToolRequest request = CallToolRequest.builder("get_contracts").arguments( |
| 85 | + Map.of("path", examplePath("Contracts.java"), "signature", "examples.Contracts.increment(int)") |
| 86 | + ).build(); |
| 87 | + CallToolResult result = client.callTool(request); |
| 88 | + assertFalse(result.isError(), result.toString()); |
133 | 89 | } |
134 | 90 |
|
135 | 91 | @Test |
136 | | - void returnsContractsOverStdio() { |
137 | | - var tool = client.listTools().tools().stream() |
138 | | - .filter(candidate -> candidate.name().equals("get_contracts")).findFirst().orElseThrow(); |
139 | | - String path = Path.of("src/test/resources/examples/Contracts.java").toAbsolutePath().toString(); |
140 | | - |
141 | | - var result = client.callTool(new CallToolRequest("get_contracts", Map.of( |
142 | | - "path", path, "signature", "examples.Contracts.increment(int)"))); |
| 92 | + void checkValidityTool() { |
| 93 | + CallToolRequest request = CallToolRequest.builder("check_validity").arguments(Map.of( |
| 94 | + "variables", Map.of("x", "int"), |
| 95 | + "ghosts", Map.of(), |
| 96 | + "assumptions", List.of("x >= 0"), |
| 97 | + "conclusion", "x > 0") |
| 98 | + ).build(); |
| 99 | + CallToolResult result = client.callTool(request); |
143 | 100 | assertFalse(result.isError(), result.toString()); |
144 | | - var content = (Map<?, ?>) result.structuredContent(); |
145 | | - assertEquals(1, ((List<?>) content.get("contracts")).size()); |
146 | | - assertTrue(McpJsonDefaults.getSchemaValidator().validate(tool.outputSchema(), content).valid()); |
147 | | - |
148 | | - var invalid = client.callTool(new CallToolRequest("get_contracts", Map.of())); |
149 | | - assertTrue(invalid.isError()); |
150 | | - assertTrue(McpJsonDefaults.getSchemaValidator().validate(tool.outputSchema(), invalid.structuredContent()).valid()); |
151 | 101 | } |
152 | 102 |
|
153 | 103 | @Test |
154 | | - void checksValidityOverStdioAlongsideVerification() throws Exception { |
155 | | - var tool = client.listTools().tools().stream() |
156 | | - .filter(t -> t.name().equals("check_validity")).findFirst().orElseThrow(); |
157 | | - var arguments = Map.<String, Object>of("variables", Map.of("x", "int"), |
158 | | - "ghosts", Map.of(), "assumptions", List.of("x >= 0"), "conclusion", "x > 0"); |
159 | | - assertTrue(McpJsonDefaults.getSchemaValidator().validate(tool.inputSchema(), arguments).valid()); |
160 | | - client.callTool(verifyRequest("Valid.java")); |
161 | | - var result = client.callTool(new CallToolRequest("check_validity", arguments)); |
162 | | - assertFalse(result.isError()); |
163 | | - var content = (Map<?, ?>) result.structuredContent(); |
164 | | - assertEquals("invalid", content.get("status")); |
165 | | - assertEquals(List.of(Map.of("variable", "x", "value", "0")), content.get("counterexample")); |
166 | | - assertTrue(McpJsonDefaults.getSchemaValidator().validate(tool.outputSchema(), content).valid()); |
167 | | - var invalid = client.callTool(new CallToolRequest("check_validity", Map.of())); |
168 | | - assertTrue(invalid.isError()); |
169 | | - assertTrue(McpJsonDefaults.getSchemaValidator().validate(tool.outputSchema(), invalid.structuredContent()).valid()); |
170 | | - assertEquals(true, ((Map<?, ?>) client.callTool(verifyRequest("Valid.java")).structuredContent()).get("success")); |
| 104 | + void checkSatisfiabilityTool() { |
| 105 | + CallToolRequest request = CallToolRequest.builder("check_satisfiability").arguments(Map.of( |
| 106 | + "variables", Map.of("x", "int"), |
| 107 | + "ghosts", Map.of(), |
| 108 | + "constraints", List.of("x == 11")) |
| 109 | + ).build(); |
| 110 | + CallToolResult result = client.callTool(request); |
| 111 | + assertFalse(result.isError(), result.toString()); |
171 | 112 | } |
172 | 113 |
|
173 | 114 | @Test |
174 | | - void checksSatisfiabilityOverStdio() { |
175 | | - var tool = client.listTools().tools().stream() |
176 | | - .filter(t -> t.name().equals("check_satisfiability")).findFirst().orElseThrow(); |
177 | | - var arguments = Map.<String, Object>of("variables", Map.of("x", "int"), |
178 | | - "ghosts", Map.of(), "constraints", List.of("x == 11")); |
179 | | - assertTrue(McpJsonDefaults.getSchemaValidator().validate(tool.inputSchema(), arguments).valid()); |
180 | | - var result = client.callTool(new CallToolRequest("check_satisfiability", arguments)); |
181 | | - assertFalse(result.isError()); |
182 | | - var content = (Map<?, ?>) result.structuredContent(); |
183 | | - assertEquals("sat", content.get("status")); |
184 | | - assertEquals(List.of(Map.of("variable", "x", "value", "11")), content.get("assignment")); |
185 | | - assertTrue(McpJsonDefaults.getSchemaValidator().validate(tool.outputSchema(), content).valid()); |
186 | | - |
187 | | - var unsat = client.callTool(new CallToolRequest("check_satisfiability", Map.of( |
188 | | - "variables", Map.of("x", "int"), "ghosts", Map.of(), |
189 | | - "constraints", List.of("x > 10", "x < 5")))); |
190 | | - assertFalse(unsat.isError()); |
191 | | - assertEquals("unsat", ((Map<?, ?>) unsat.structuredContent()).get("status")); |
192 | | - |
193 | | - var invalid = client.callTool(new CallToolRequest("check_satisfiability", Map.of())); |
194 | | - assertTrue(invalid.isError()); |
195 | | - assertTrue(McpJsonDefaults.getSchemaValidator().validate(tool.outputSchema(), invalid.structuredContent()).valid()); |
| 115 | + void getStateMachineTool() { |
| 116 | + CallToolRequest request = CallToolRequest.builder("get_state_machine").arguments( |
| 117 | + Map.of("path", examplePath("StateMachine.java")) |
| 118 | + ).build(); |
| 119 | + CallToolResult result = client.callTool(request); |
| 120 | + assertFalse(result.isError(), result.toString()); |
196 | 121 | } |
197 | 122 |
|
198 | | - private static CallToolRequest verifyRequest(String example) { |
199 | | - String path = Path.of("src/test/resources/examples", example).toAbsolutePath().toString(); |
200 | | - return new CallToolRequest("verify", Map.of("path", path)); |
| 123 | + private static String examplePath(String example) { |
| 124 | + return Path.of("src/test/resources/examples", example).toAbsolutePath().toString(); |
201 | 125 | } |
202 | 126 | } |
0 commit comments