请不要在理科生面前炫耀自己的某些生理能力!切记!

海魔

刚学了形式化，那么就用形式化来证明楼猪ML行为的正确姓。
　　　　　　　　以下用到进程代数
　　　　　　　　用进程JJ代表楼猪JJ
　　　　　　　　用进程MM代表楼猪MM
　　　　　　　　用in代表入，out代表出，open代表开，close代表合
　　　　　　　　那么
　　　　　　　　JJ=a->b->c->d->JJ;
　　　　　　　　MM=a->b->c->d->MM;
　　　　　　　　JJ||MM表示进程的并行执行。
　　　　　　　　那么JJ||MM=uX.(a->b->c->d->X);
　　　　　　　　经验证其间不会发生死锁，楼猪可以放心。另停机问题还不知道怎么验证？也就是缺少完全正确姓的证明。