From 7cbe538e14b655e8786d8787e438fdd7a7393d8d Mon Sep 17 00:00:00 2001
From: LudwigVonChesterfield
 <17705613+LudwigVonChesterfield@users.noreply.github.com>
Date: Wed, 24 Sep 2025 21:03:57 -0400
Subject: [PATCH] adds specification formatting for ground truth of 2011
 Finding Maximum in an Array problem

---
 src/two_k_11/challenge1.rs | 36 ++++++++++++++++++++++++++++++++++--
 1 file changed, 34 insertions(+), 2 deletions(-)

diff --git a/src/two_k_11/challenge1.rs b/src/two_k_11/challenge1.rs
index feee794..451487d 100644
--- a/src/two_k_11/challenge1.rs
+++ b/src/two_k_11/challenge1.rs
@@ -2,12 +2,44 @@ use vstd::prelude::*;
 
 verus! {
 
+//datastructures
+// TO-DO: why do we specify these? For Tree-like problems?
+// [i32]
+//enddatastructures
+
+//preconditions
+// Encodes: A non-empty integer array a.
+pub fn precondition1(a: &[i32]) -> bool {
+    0 < a.len() <= usize::MAX
+}
+//endpreconditions
+
+//postconditions
+// TO-DO: Wonder how we'll make the signatures compatible.
+// Encodes: index re-turned by the method max() points to an element maximal in the array.
+pub fn postcondition1(a: &[i32], max_idx: usize) {
+    forall|i: int| 0 <= i < a.len() ==> a[max_idx as int] >= a[i]
+}
+//endpostconditions
+
+//specs
+spec pub fn preconditions(a: &[i32]) -> bool {
+    precondtion1(a)
+}
+
+spec pub fn postconditions(a: &[i32], max_idx: usize) {
+    postcondition1(a, max_idx)
+}
+//endspecs
+
 #[allow(unused)]
+//signature
 pub fn max(a: &[i32]) -> (max_idx: usize)
+//endsignature
     requires
-        0 < a.len() <= usize::MAX,
+        preconditions(a),
     ensures
-        forall|i: int| 0 <= i < a.len() ==> a[max_idx as int] >= a[i],
+        postconditions(a, max_idx),
 {
     let mut x = 0usize;
     let mut y = a.len() - 1;