1. 用户注册与登入

• 用户注册:

   系统首页中，切换至【注册】区域，输入对应用户信息，进行注册；需要用户提供最基本的信息，如：注册账号，用户名，密码，以及邮箱。

• 匿名用户登入

   匿名用户可以有两种方式进行登入，具体位置如下：
   方式一：登入界面


   方式二：登入界面

   匿名登入的情况下，可以在线编辑程序，进行验证，并对验证结果进行确认。
   匿名登入的用户无法对提交验证的程序和验证结果进行保存。而以注册用户身份登入使用时，系统将保留提交的验证程序及对应的验证结果。

• 注册用户登入

   新用户注册完成后，初次登入时，需要输入注册邮箱中收到的验证码。
   成功激活后，进入程序验证主画面，对于已经激活的用户，后续再次登入时，不再要求提供验证码。
   注册用户首次登入主画面时，系统会为用户默认创建一个名为“untitled.c”的空白程序文件。
   以后登入时，系统将显示保存的文件列表，打开上次登出时的验证程序和该文件最近一次的验证结果，例如：

• 用户密码重置

   登入界面中点击【忘记密码】按钮，可以进行用户密码的重置。
   填写注册时提供的邮箱地址，用来接收密码重置的验证信息。
   验证信息发送成功后，查看邮箱中相关的验证码信息。
   输入验证邮件中的验证码，以及新密码，点击确认按钮，完成密码重置操作。

2. 文件相关功能

• 文件添加

   注册用户登入的情况下，点击左上侧文件处理图标，在弹出的文件菜单中点击【添加程序文件】，进行程序文件的添加，创建一个新的验证程序。

• 本地文件装载

   注册用户登入的情况下，点击左上侧文件处理图标，在弹出的文件菜单中点击【装载本地文件】，进行本地程序文件的上传和添加。新添加的文件内容与本地文件内容一致。
   通过文件选择对话框进行本地文件的选择。
   各个浏览器显示的对话框可能不相同，以下以Chrome（谷歌）浏览器为例，表示相关内容

   点击【打开】按钮，选择需要上传的文件，这里选择“maxInArray.c”作为演示。本地文件上传处理成功后，文件列表中则会显示相应的记录。
   对于出现重复的情况，需要提供新的文件名，通过对新添加的文件进行重新命名，完成文件的上传和添加。
   上传成功时，文件名在文件列表中当前光标所在的位置。以后界面刷新时，文件列表将按字母序升序排序。

• 注册用户所有文件打包下载

   注册用户登入的情况下，点击左上侧文件处理图标，在弹出的文件菜单中点击【打包下载所有文件】，用户当前文件列表中的所有程序文件将打包下载到浏览器的缺省下载目录。

• 文件重命名

   鼠标悬停在文件列表中的文件名上，左侧出现文件操作图标。点击图标，在弹出的文件菜单中点击【重命名】按钮，进行文件的重命名操作。

   重命名对话框中，输出新的文件名，点击【保存】按钮，进行当前选中文件的重命名。文件名的长度为64字符。

• 文件下载

   鼠标悬停在文件列表中的文件上，点击文件操作图标，在弹出的文件菜单中点击【下载】按钮，进行文件的下载操作。文件将下载到浏览器的缺省下载目录。

• 文件删除

   鼠标悬停在文件列表中的文件上，点击文件操作图标 ，在弹出的文件菜单中点击【删除】按钮，进行文件的删除操作。
注：文件删除后无法进行恢复，请在详细确认无误后再进行删除操作。

• 文本编辑器

   主画面的中间区域为验证程序的编辑区，用户可以创建新文件，或对添加、上传的文件进行编辑。

• 程序文件提交服务器

   修改后的程序文件，通过点击【保存】按钮，或者编辑区域的邮件菜单中的【Save】选项，或者使用快捷键“Ctrl + S”进行文件的上传保存。

3. 程序验证功能

• 验证开始

   点击编辑区域右上角的【验证】按钮，启动程序验证。
   在点击验证按钮前，如果当前选中文件存在变更，系统将提示是否保存当前文件内容。点击【保存】按钮后，执行文件保存并启动验证处理。

   对于已经存在验证结果文件，且文件内容已修改的情况，系统将额外提示保存动作会引起最近一次验证结果的删除，确认是否保存。
   点击【保存】按钮后，执行文件保存、清空最近一次验证结果并启动验证处理。

   启动验证处理后，编辑区域会进入验证处理中状态。
   程序文件验证完成时，提示验证已经完成，并恢复主画面的状态至验证前。

• 验证结果查看

   验证结果有概要验证结果和详细验证结果两个区域组成。
   1.概要结果显示汇总后的验证结果
      通过选中概要结果中的记录，切换详细验证结果中的信息。
      切换验证结果右侧的下拉框选项，对结果进行筛选显示

   2.2. 详细结果由四个部分组成，错误检查、验证结果、语言演算和引理证明。
   具体显示如下
   错误检查

   验证结果

   验证结果中的形状图显示

   点击【SVG】按钮，查看形状图，形状图显示效果如下：
   形状图SVG1

   形状图中显示对应的断言状态，并以图的方式进行呈现。
   SVG2

   语句演算

   引理证明

4. 帮助和反馈

• 帮助

   主画面中点击左上角的【帮助】按钮，在弹出的菜单中可以打开在线文档网页。
   在线文档主要是系统相关的使用手册和样例程序，项目有安全C使用手册、安全C规范语言SCSL使用手册和验证程序样例三个选项

• 问题反馈

   主画面中点击左上角的【问题反馈】按钮，就可以在弹出的弹框中反馈遇到的问题。