Initial revision.halt3-1.0

5 files changed, 152 insertions, 0 deletions

diff --git a/example-error-decider.c b/example-error-decider.c
new file mode 100644
index 0000000..89a2e3e
--- /dev/null
+++ b/example-error-decider.c
@@ -0,0 +1,4 @@
+int error_decider(const char *hdecider, const char *program, const char *input)
+{
+  return 1;
+}
diff --git a/example-halting-decider.c b/example-halting-decider.c
new file mode 100644
index 0000000..101bf05
--- /dev/null
+++ b/example-halting-decider.c
@@ -0,0 +1,6 @@
+#include "ternary.h"
+
+ternary halting_decider(const char *program, const char *input)
+{
+  return ERROR;
+}
diff --git a/genprog.sh b/genprog.sh
new file mode 100755
index 0000000..b3d4d3f
--- /dev/null
+++ b/genprog.sh
@@ -0,0 +1,123 @@
+#!/bin/sh
+
+#
+# This script requires two arguments which are file names:
+#
+# 1. The name of a C source file which defines a three-valued halting
+#    decider function, whose prototype is:
+#
+#      ternary halting_decider(const char *program, const char *input);
+#
+#    This function tries to answer the question: does the program,
+#    when given the specified input, halt? It can return TRUE, or FALSE.
+#    It can also return ERROR when, for whatever reason, it deems
+#    that neither TRUE nor FALSE is the correct answer.
+#
+# 2. The name of a C source file which defines the following boolean
+#    function, which returns 0 or 1:
+#
+#      int error_decider(const char *hdecider, const char *program,
+#                        const char *input);
+#
+#    Error decider functions try to answer the question: does the given
+#    program, when operating on the given input, behave in such
+#    a way that the given decider must return ERROR for that program?
+#
+
+set -e # stop on any errors
+
+MYDIR=$(dirname "$0")
+
+. "$MYDIR"/lib.sh
+
+if [ $# != 2 ] ; then
+  printf "usage: $0 <halting_decider>.c <error_decider.c>\n"
+  exit 1
+fi
+
+ORIG_HALTING_DECIDER=$1
+ORIG_ERROR_DECIDER=$2
+
+HD_FULL_HASH=$(file_hash $ORIG_HALTING_DECIDER)
+ED_FULL_HASH=$(file_hash $ORIG_ERROR_DECIDER)
+HD_HASH=$(short_hash $HD_FULL_HASH)
+ED_HASH=$(short_hash $ED_FULL_HASH)
+
+HALTING_DECIDER=hd-${HD_HASH}.c
+ERROR_DECIDER=ed-${ED_HASH}.c
+
+cp $ORIG_HALTING_DECIDER $HALTING_DECIDER
+cp $ORIG_ERROR_DECIDER $ERROR_DECIDER
+
+PROGRAM_BASENAME=pg-${HD_HASH}-${ED_HASH}
+
+printf "halting decider: %s\n" $HALTING_DECIDER
+printf "error decider: %s\n" $ERROR_DECIDER
+printf "\n"
+printf "generating program %s from these deciders\n" $PROGRAM_BASENAME.c
+
+cat > ${PROGRAM_BASENAME}.c <<!
+#include <stdio.h>
+#include <stdlib.h>
+#include "ternary.h"
+
+#define HD_HASH "$HD_HASH"
+#define ED_HASH "$ED_HASH"
+#define PG_BASE "$PROGRAM_BASENAME"
+#define PG_SELF PG_BASE ".c"
+#define HD_NAME "$HALTING_DECIDER"
+
+#include "$ERROR_DECIDER"
+#include "$HALTING_DECIDER"
+
+int main(int argc, char **argv)
+{
+  const char *input;
+
+  if (argc != 2) {
+    fprintf(stderr, "this program test case requires input\n");
+    return EXIT_FAILURE;
+  }
+
+  input = argv[1];
+
+  if (error_decider(HD_NAME, PG_SELF, input)) {
+    switch (halting_decider(PG_SELF, input)) {
+    case FALSE:
+      printf("decider %s RIGHT: %s/%s does not halt\n", HD_NAME, PG_SELF, input);
+      for(;;);
+    case TRUE:
+      printf("decider %s RIGHT: %s/%s halts\n", HD_NAME, PG_SELF, input);
+      return EXIT_SUCCESS;
+    case ERROR:
+      printf("decider %s WRONG: TRUE and FALSE are viable answers for %s/%s\n",
+             HD_NAME, PG_SELF, input);
+      abort();
+    }
+  } else {
+    switch (halting_decider(PG_SELF, input)) {
+    case FALSE:
+      printf("decider %s WRONG: %s/%s does not halt\n", HD_NAME, PG_SELF, input);
+      return EXIT_SUCCESS;
+    case TRUE:
+      printf("decider %s WRONG: %s/%s halts\n", HD_NAME, PG_SELF, input);
+      for(;;);
+    case ERROR:
+      printf("decider %s RIGHT: neither TRUE nor FALSE is correct for %s/%s\n",
+             HD_NAME, PG_SELF, input);
+      abort();
+    }
+  }
+  /* notreached */
+  puts("internal error");
+  abort();
+}
+!
+
+printf "compiling %s to %s\n" $PROGRAM_BASENAME.c $PROGRAM_BASENAME
+gcc $PROGRAM_BASENAME.c -o $PROGRAM_BASENAME
+
+printf "\n"
+
+printf "executing test case %s %s\n" ./$PROGRAM_BASENAME $PROGRAM_BASENAME
+./$PROGRAM_BASENAME $PROGRAM_BASENAME
diff --git a/lib.sh b/lib.sh
new file mode 100644
index 0000000..08da993
--- /dev/null
+++ b/lib.sh
@@ -0,0 +1,13 @@
+#
+# Library of functions
+#
+
+file_hash()
+{
+   sha256sum $1 | awk '{ print $1 }'
+}
+
+short_hash()
+{
+   awk "BEGIN { print substr(\"$1\", 1, 7) }"
+}
diff --git a/ternary.h b/ternary.h
new file mode 100644
index 0000000..0711fec
--- /dev/null
+++ b/ternary.h
@@ -0,0 +1,6 @@
+#ifndef TERNARY_H
+#define TERNARY_H
+
+typedef enum { FALSE, TRUE, ERROR } ternary;
+
+#endif