数组最小和截断问题
数组最小和截断（Minimal Sum Section）问题是指：给出整数数组a[0..n-1]，求所有数组片段中和最小者。即 Min(a[i]+a[i+1]+...+a[j] | 0 <= i <= j <= n-1)。
（验证时间约3sec）
算法及程序实现请见《面向计算机科学的数理逻辑-系统建模与推理》（Michael Huth和Mark Ryan著，何伟 樊磊译，机械工业出版社）一书 P189。
[Back to Index]
验证特点： 逻辑函数，存在量词，全称量词
标注说明：函数前条件：给出数组a的一般性质和数组元素的取值范围；
函数后条件：数组a存在一个片段和等于函数返回值，且返回值小于等于数组a的所有片段和。
程序样例 
