pairsSumToZero

program-simple.bat

; Based on https://markushimmel.de/blog/my-first-verified-imperative-program/
(defrule sum-is-0
	(list $? ?first $? ?second $?)
	(test (= 0 (+ ?first ?second)))
	=>
	(println TRUE))

(defrule sum-is-not-0
	(not (and
		(list $? ?first $? ?second $?)
		(test (= 0 (+ ?first ?second)))))
	=>
	(println FALSE))

(assert (list 1 0 2 -1))
(run)
(exit)

program.bat

; Based on https://markushimmel.de/blog/my-first-verified-imperative-program/
(defrule sum-is-0
	(list $?before ?first $?middle ?second $?)
	(test (= 0 (+ ?first ?second)))
	=>
	(println "List has two values that sum to 0:")
	(println ?first " (index " (length$ ?before) "), " ?second " (index " (+ 1 (length$ ?before) (length$ ?middle)) ")"))

(defrule sum-is-not-0
	(not (and
		(list $?before ?first $?middle ?second $?)
		(test (= 0 (+ ?first ?second)))))
	=>
	(println "List does not have two values that sum to 0 :("))

(reset)
(assert (list 1 0 2 -1))
(println "Test 1")
(run)
(println)

(reset)
(assert (list 3 0 2 -1))
(println "Test 2")
(run)
(println)

(reset)
(assert (list 3 0 2 -1 4 9 2 1 -2))
(println "Test 3")
(run)
(println)

(reset)
(assert (list 7 0 2 -1 4 9 2 1 -8 32 -4 7 2))
(println "Test 4")
(run)
(println)
(exit)