PAT——一种高性能软件验证工具

通信顺序进程（communicating sequential proces）验证软件，打开csp格式文件的软件，对开发的软件进行验证的高性能工具。

//the namespace must be PAT.Lib the class and method names can be arbitrary
namespace PAT.Lib
{
    /// 

    /// You can use static library in PAT model.
    /// All methods should be declared as public static.
    /// 
    /// The parameters must be of type “int“ “bool“ “int[]“ or user defined data type
    /// The number of parameters can be 0 or many
    /// 
    /// The return type can be void bool int int[] or user defined data type
    /// 
    /// The method name will be used directly in your model.
    /// e.g. call（max 10 2） call（dominate 3 2） call（amax [135]）
    /// 
    /// Note: method names are case sensetive
    /// 

    public class Array
    {
        /// 

        /// Return the length of the array
        /// 

        /// 
        /// 
        public static int ArrayLength（int[] array）
        {
            return array.Length;
        }

        /// 

        /// Test whether the array is of size 0 or not
        /// 

        /// 
        /// 
        public static bool IsArrayEmpty（int[] array）
        {
            return array.Length == 0;
        }

        /// 

        /// Return the max element in an array
        /// 

        /// 
        /// 
        public static int ArrayMax（int[] array）
        {
            int max = array[0];
            foreach （int v in array）
            {
                if （max < v）
                {
                    max = v;
                }
            }
            return max;
        }

        /// 

        /// Return the min element in an array
        /// 

        /// 
        /// 
        public static int ArrayMin（int[] array）
        {
            int min = array[0];
            foreach （int v in array）
            {
                if （min > v）
                {
                    min = v;
                }
            }
            return min;
        }
    }
}

 属性            大小     日期    时间   名称
----------- ---------  ---------- -----  ----
     文件      281600  2012-12-28 22:25  Microsoft.Msagl.dll
     文件      101888  2012-12-28 22:25  Microsoft.Msagl.Drawing.dll
     文件      143872  2012-12-28 22:25  Microsoft.Msagl.GraphViewerGdi.dll
     文件       86016  2012-12-28 22:25  Microsoft.VisualStudio.TextTemplating.dll
     文件      423784  2012-12-28 22:25  office.dll
     文件     4668928  2012-12-28 22:25  PAT 3.exe
     文件        4083  2012-12-28 22:28  PAT 3.ini
     文件     2071040  2012-12-28 22:25  PAT.Common.dll
     文件     2007040  2012-12-28 22:25  PAT.Editor.Core.dll
     文件      356352  2012-12-28 22:25  PAT.Editor.dll
     文件      413696  2012-12-28 22:25  PAT.Editor.Docking.dll
     文件       95744  2012-12-28 22:25  PAT.Launcher.exe
     文件         144  2012-12-28 22:25  PAT.Launcher.exe.config
     文件      206848  2012-12-28 22:25  PAT.Update.exe
     文件       21504  2012-12-28 22:25  PAT3.Console.exe
     文件         141  2012-12-28 22:25  PATEnv.bat
     文件          12  2012-12-28 22:28  recents.xml
     文件       45056  2012-12-28 22:25  Uninstall.exe
     文件       45056  2012-12-28 22:25  VBE6EXT.OLB
     目录           0  2012-12-28 22:28  de\
     文件      340992  2012-12-28 22:25  de\PAT 3.resources.dll
     文件       32256  2012-12-28 22:25  de\PAT.Common.resources.dll
     目录           0  2012-12-28 22:28  Docs\
     文件     4244840  2012-12-28 22:25  Docs\Help.chm
     文件       22565  2012-12-28 22:25  Docs\pat.sty
     目录           0  2012-12-28 22:28  Examples\
     目录           0  2012-12-28 22:28  Examples\UML Examples\
     文件        4050  2012-12-28 22:25  Examples\UML Examples\ATM.xmi
     文件        1995  2012-12-28 22:25  Examples\UML Examples\basic.xmi
     文件        5588  2012-12-28 22:25  Examples\UML Examples\fork&Join.xmi
     文件        4242  2012-12-28 22:25  Examples\UML Examples\orthogonal.xmi
............此处省略88个文件信息