[ヤマト運輸 おせち約1200個届けられず 冷凍と冷蔵誤る]
宅配便最大手のヤマト運輸が北海道向けにおせち料理を配送する際、本来、冷凍で運ぶところを誤って冷蔵で運搬し、1200個余りのおせち料理を届けられなかったことがわかりました。
http://www3.nhk.or.jp/news/html/20181231/k10011764351000.html
逆は無理だし vivaldi の機能か
Vivaldi から chrome へタブを drag'n'drop できてびっくりしてる
件の記事で使われていたVDM以外だとAlloy、SMV、SPIN、Z言語辺りが似たようなモデル検査プロジェクトで使われる道具として有名
Alloyなどでmodel checkingするのもformal methodで、たとえばCoqでextractしないとformal methodじゃないというわけではないと私は思っています
Formal Method といいつつ仕様記述だけなのか / "自動改札機の運賃計算プログラムはいかにデバッグされているのか? 10の40乗という運賃パターンのテスト方法を開発者が解説(後編) - Publickey"
https://www.publickey1.jp/blog/12/_1040_2.html
自動改札機の運賃計算プログラムはいかにデバッグされているのか? 10の40乗という運賃パターンのテスト方法を開発者が解説(後編) - Publickey https://www.publickey1.jp/blog/12/_1040_2.html
自動改札機の運賃計算プログラムはいかにデバッグされているのか? 10の40乗という運賃パターンのテスト方法を開発者が解説(中編) - Publickey https://www.publickey1.jp/blog/12/_1040_1.html
私は電子書籍を滅多に買わない紙書籍派だけど、物体は空間というコストを手放すまでずっと支払わせ続けるという面はあって、悩まされている現状がある
自動改札機の運賃計算プログラムはいかにデバッグされているのか? 10の40乗という運賃パターンのテスト方法を開発者が解説(前編) - Publickey https://www.publickey1.jp/blog/12/_1040.html
流石!
QT:・・ところで皆さんご存じかもしれませんが、YouTubeには違法な「動画化マンガ」が結構アップロードされています。
※ 違法な動画化マンガの一例:「バキ21巻」 *1
先日、とうとう逮捕者も出ましたが、今でも多くの動画化マンガがYouTubeにアップロードされ続けていますね。中でもBL(ボーイスラブ)漫画の閲覧数は非常に多いようです。これは恐らく、儲かるか、もしくは反響が大きくて面白いのでしょう。
じゃあこれを公式が合法的にやってみよう!・・・というのが発想の原点です。
【新サービスの実験】マンガを全自動でYouTubeの動画に変換し、セリフも100カ国語に自動翻訳して、海外でもどんどん読んでもらおう! - (株)Jコミックテラスの中の人
https://kenakamatsu.hatenablog.com/entry/2018/12/30/223548
ポケモンGoの起動画面、もう2019の表示になったんだけど。