📄 spark95.txt
字号:
/L20 "SPARK95" Line Comment Num = 3-- Block Comment On Alt = -- Block Comment Off Alt = # String Chars = " File Extensions = ADS ADB ADA
/Delimiters =" ,();'
/Indent Strings = "begin"
/Unindent Strings = "end"
/Function String = "^(%[ \t]+^{function^}^{procedure^}*$^)"
/Function String 1 = "^(%^{function^}^{procedure^}*$^)"
/Function String 2 = "^[ \t]*(procedure|function)(.*)(is|;|)[ \t]*$"
/C1"Strings and Chars"
"
/C2"Ada95 Keywords & SPARK Allowed Attributes"
abort abs abstract accept access aliased all and array at
Adjacent Aft
begin body
Base
case constant
Ceiling Component_Size Compose Copy_Sign
declare delay delta digits do
Delta Denorm Digits
else elsif end entry exception exit
Exponent
for function
First Floor Fore Fraction
generic goto
if in is
Identity Image Input
limited loop
Last Leading_Part Length
mod
Machine Machine_Emax Machine_Emin Machine_Mantissa Machine_Overflows Machine_Radix Machine_Rounds Max
Min Model Model_Emin Model_Epsilon Model_Mantissa Model_Small
new not null
of or others out
package pragma private procedure protected
Pos Pred
raise range record rem renames requeue return reverse
Read Remainder Rounding
select separate subtype
Safe_First Safe_Last Scaling Signed_Zeros Size Small Succ
tagged task terminate then type
Truncation
until use
Unbiased_Rounding
Val Valid
when while with
xor
/C3"SPARK Keywords"
assert
check
derives
from
global
hide hold
inherit initializes invariant
main_program
own
post pre
some
/C4"Forbidden Attributes"
Access Address Alignment
Bit_Order Body_Version
Callable Caller Class Constrained Count
Definite
External_Tag
First_Bit
Last_Bit
Max_Size_In_Storage_Elements
Modulus
Output
Partition_Id Position
Range Round
Scale Storage_Pool Storage_Size
Tag Terminated
Unchecked_Access
Value Version
Wide_Image Wide_Value Wide_Width Width Write
/C5"FDL Words"
are_interchangeable as assume
const
div
element
finish first for_all for_some
goal
last
may_be_deduced may_be_deduced_from may_be_replaced_by
nonfirst nonlast not_in
odd
pending pred proof
requires
save sequence set sqr start strict_asubset_of subset_of succ
update
var
where
⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -