博文
B Machine
|||
MACHINE
container(ELEMS)
VARIABLES
elems
INVARIANT
elems<:POWE(ELEMS)
INITIALISATION
elems:={}
OPERATIONS
insert(ex)
PRE
ex<:elems
THEN
elems:=elems UNION {ex}
END;
ex<-peek=
PRE
elems/:{}
THEN
ex:<:elems
END;
ex<-take=
PRE
elems/={}
THEN
ex:<:elems||
elems:=elems-{ex}
END
END//状态机结束
注释：
变量之间用“,”分隔
不变式谓词之间用“&”连接
操作之间用“；”连接
https://blog.sciencenet.cn/blog-794010-639664.html
上一篇：Virtuoso数据库访问
下一篇：在Virtuoso中使用Sparql
