Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
[B! mcu][proof] masterqのブックマーク
[go: Go Back, main page]

タグ

mcuとproofに関するmasterqのブックマーク (1)

  • ATS で組み込みドライバを実装してみる③ - でんちゅーがらす

    「――何かを怠けるのに、理由が要るかい?」 はい、ATSでRXの端子ドライバを書いてみる③。今回で最終回です。 今回は、今まで準備してきた道具を使って、端子を操作する簡単なプログラム(証明付き)を書いてみます。 仕様 まずは、どんなプログラムを書くのかを決めねばなりません。↓のようなものを目指します。 ① 起動する。 ② P00端子に500ミリ秒間Highを出力する。 ③ P00端子に250ミリ秒間Lowを出力する。 ④ P00端子に400ミリ秒間Highを出力する。 ⑤ P00端子にLowを出力する。 ⑥ 終了する。 端子の番号は(見てわかる通り)適当です。もし、この端子の先にLEDが繋がっていれば、それが2回点灯することになります。いわゆるLチカです。 では次に、この仕様を型によって表現します。そのためにいくつか新しい定義を行います。 出力履歴 datasort output_dura

    ATS で組み込みドライバを実装してみる③ - でんちゅーがらす
    masterq
    masterq 2018/10/09
    "「ATSはそういう言語じゃないぞ」というのが正解なのだと思います。簡単な型注釈だけを使って、本格的な証明が必要なときはpraxiでも使ってごまかせば良い、というのが本来の使い方"
  • 1