尝试执行代码块时遇到一个奇怪的问题（尤其是 Java 中的 ProcessBuilder 类）
有效的代码：
package modules.user.verify;
import java.io.*;
import java.util.*;
import java.net.*;
public class VerifyUser {
public static void main(String[] args) {
boolean listening = true;
try {
ServerSocket server = new ServerSocket(20002);
while(listening) {
Socket client = server.accept();
PrintWriter out = new PrintWriter(client.getOutputStream(), true);
BufferedReader in = new BufferedReader(new InputStreamReader(client.getInputStream()));
String input, store = "", request = "";
// For all input received, write it to the request buffer.
while((input = in.readLine()) != null) {
request += input;
} // end while loop
BufferedReader reader = new BufferedReader(new FileReader("store/address-book/address-book.xml"));
while((input = reader.readLine()) != null) {
store += input;
} // end while loop
String acl2 = "(include-book \"modules/user/verify/verify-user\")" +
"(in-package \"ACL2\")" +
"(set-state-ok t)" +
"(set-guard-checking :none)" +
"(testUser \"" + request + "\" \"" + store + "\" state)";
System.out.println("Executing ACL2 runtime...");
ProcessBuilder processBuilder = new ProcessBuilder("acl2");
File log = new File("logs/user/verify/acl2_log.txt");
processBuilder.redirectErrorStream(true);
processBuilder.redirectOutput(ProcessBuilder.Redirect.appendTo(log));
Process process = processBuilder.start();
PrintWriter procIn = new PrintWriter(process.getOutputStream());
// Write the ACL2 to the process, exit ACL2 and close the socket
procIn.println(acl2);
procIn.println("(good-bye)");
procIn.flush();
procIn.close();
out.close();
in.close();
client.close();
} // end while loop
server.close();
System.exit(0);
} catch(Exception e) {
e.printStackTrace();
} // end try/catch
} // end function main
} // end class VerifyUser
不起作用的代码：
package modules.user.register;
import java.io.*;
import java.util.*;
import java.net.*;
public class RegisterUser {
public static void main(String[] args) {
boolean listening = true;
try {
// Acquire the listening port for connection to client.
ServerSocket server = new ServerSocket(20001);
while(listening) {
// Wait until the client connects
Socket client = server.accept();
// Handles for input and output streams relating to the socket connection
PrintWriter out = new PrintWriter(client.getOutputStream(), true);
BufferedReader in = new BufferedReader(new InputStreamReader(client.getInputStream()));
// Buffers
String input, store="", request="";
// Read the input from the connection
while((input = in.readLine()) != null) {
request += input;
} // end while
// Read the contents of the address-book currently stored
BufferedReader reader = new BufferedReader(new FileReader("store/address-book/address-book.xml"));
while((input = reader.readLine()) != null) {
store += input;
} // end while
// The ACL2 code to execute.
String acl2 = "(include-book \"register-user\")" +
"(in-package \"ACL2\")" +
"(registerUser \"" + request + "\" \"" + store + "\" state)";
// Initialize ACL2 and dump its output to the log
System.out.println("Executing ACL2 runtime for RegisterUser...");
ProcessBuilder processBuilder = new ProcessBuilder("acl2");
File log = new File("logs/user/register/acl2_log.txt");
processBuilder.redirectErrorStream(true);
processBuilder.redirectOutput(ProcessBuilder.Redirect.appendTo(log));
Process process = processBuilder.start();
PrintWriter procIn = new PrintWriter(process.getOutputStream());
// Write the ACL2 to the process, close ACL2
//procIn.println(acl2);
//procIn.println("(good-bye)");
//procIn.flush();
//procIn.close();
// Old store is old address-book file and new store is newly generated
File oldStore = new File("store/address-book/address-book.xml");
File newStore = new File("store/address-book/temp_address-book.xml");
// Response header information
String response = "<?xml version='1.0'?>" +
"<!DOCTYPE response SYSTEM 'dtd/reponse.dtd'>" +
"<response>";
// Determine if there was a change.
// If entry was added, the length > that old length.
if(oldStore.length() < newStore.length()) {
// Replace old file with new file
oldStore.delete();
newStore.renameTo(oldStore);
// Extract data from request XML
String name = request.substring(request.indexOf("<name>")+6, request.indexOf("</name>")-7);
String domain = request.substring(request.indexOf("<domain>")+8, request.indexOf("</domain>")-9);
// Create the store directory for the user's emails
File storeDirectory = new File("store/email/" + domain + "/" + name + "/");
storeDirectory.mkdirs();
response += "<message>ACCEPT</message>";
} else {
// Remove new file as it is pointless
newStore.delete();
response += "<message>REJECT</message>";
} // end if-else
response += "</response>";
// Writeback the response to the client
out.print(response);
out.flush();
// Close all streams
out.close();
in.close();
client.close();
} // end while
} catch(Exception e) {
e.printStackTrace();
} // end try/catch
} // end function main
} // end class RegisterUser
如您所见，我没有向程序传递任何参数。当我在 Windows DOS shell 上回显 %PATH% 时，它显示 C:\ACL2 在我的 ENV vars 中（这是 acl2.exe 所在的文件夹）。我尝试将 acl2 更改为 C:\ACL2\acl2.exe 只是为了得到相同的结果。
令我惊讶的是为什么第一个工作完美而第二个（具有几乎相同的完全相同的代码 - 完全相同的 ProcessBuilder 代码）不起作用。
看来这段代码是我的问题所在：
System.out.println("Executing ACL2 runtime...");
ProcessBuilder processBuilder = new ProcessBuilder("acl2");
File log = new File("logs/user/register/acl2_log.txt");
processBuilder.redirectErrorStream(true);
processBuilder.redirectOutput(ProcessBuilder.Redirect.appendTo(log));
Process process = processBuilder.start();
PrintWriter procIn = new PrintWriter(process.getOutputStream());
错误：
Executing ACL2 runtime for RegisterUser...
java.io.IOException: Cannot run program "acl2": The system cannot find the path specified
at java.lang.ProcessBuilder.start(Unknown Source)
at modules.user.register.RegisterUser.main(RegisterUser.java:74)
Caused by: java.io.IOException: The system cannot find the path specified
at java.lang.ProcessImpl.openForAtomicAppend(Native Method)
at java.lang.ProcessImpl.newFileOutputStream(Unknown Source)
at java.lang.ProcessImpl.start(Unknown Source)
... 2 more
应该发生的是，启动的进程是 ACL2 环境，代码被发送到它被执行，然后进程被杀死（通过 ACL2 中的（再见）命令）。之后代码应该在一点点Java之后退出，这与发生错误的ACL2进程无关。
VerifyUser 程序调用 ACL2，将响应写入“server-response.xml”文件并正常退出而不会发生任何事件。
RegisterUser 程序应该调用 ACL2，写一个响应并优雅地退出，一个小的 java 代码为用户创建一个目录，删除一个存储文件并重命名新生成的用户注册。