commit ce7260449861cf453199c66c940bbe0f4ce69f60
parent 79236ea87082ff76badfc09257a037b72b9c8655
Author: Jan Pobrislo <ccx@te2000.cz>
Date: Sun, 11 May 2025 23:48:44 +0000
WIP specification of program behavior
Diffstat:
1 file changed, 21 insertions(+), 0 deletions(-)
diff --git a/doc/miniroon_spec.pl b/doc/miniroon_spec.pl
@@ -76,6 +76,7 @@ will_be(Value, Goal) :-
freeze(Value, assertion(call(Goal, Value))).
byte(Value) :- must_be(between(0, 255), Value).
+nonzero_byte(Value) :- must_be(between(1, 255), Value).
nonnegative_integer(Value) :- must_be(nonneg, Value).
@@ -84,6 +85,13 @@ sequence_of_bytes([First|Rest]) :-
First will_be byte,
Rest will_be sequence_of_bytes.
+sequence_of_nonzero_bytes([]).
+sequence_of_nonzero_bytes([First|Rest]) :-
+ First will_be nonzero_byte,
+ Rest will_be sequence_of_nonzero_bytes.
+
+file_path(X) :- sequence_of_nonzero_bytes(X).
+
%%% Generic grammar definitions:
nonzero_digit(Code) -->
@@ -173,3 +181,16 @@ miniroon_v0_caveat_list([]) --> {true}.
miniroon_v0_caveat_list([Caveat|Rest]) -->
netstring_call_dcg(miniroon_v0_caveat(Caveat)),
miniroon_v0_caveat_list(Rest).
+
+miniroon_is_catdir(CatalogDirectory) :- assertion(false). % TODO
+miniroon_is_rundir(RunDirectory) :- assertion(false). % TODO
+miniroon_is_environ(ExecutionEnvironment) :- assertion(false). % TODO
+miniroon_is_verdict(deny).
+miniroon_is_verdict(allow(Program, ResultEnvironment)) :-
+ miniroon_is_environ(ResultEnvironment),
+ file_path(Program).
+miniroon_read_execution(InitialEnvironment, CatalogDirectory, Input, Verdict) :-
+ miniroon_is_environ(InitialEnvironment),
+ miniroon_is_catdir(CatalogDirectory),
+ Verdict will_be miniroon_is_verdict,
+ assertion(false). % TODO