たれぱんのびぼーろく

わたしの備忘録、生物学とプログラミングが多いかも

Raspberry Pi Zero WをBluetooth経由で操作する

sshみたいなノリで、Bluetooth経由のRPiリモートアクセスを可能にする。

概要

Bluetooth上でシリアル通信をおこない、シリアル通信のRaspberry Pi側終端をagettyにつなぐことでリモートアクセスを可能にする。
BluetoothdのUnitを少しいじり、rfcomm->agettyのdaemon用Unitをかけば、立ち上げ時に自動で受け入れ態勢をONにできる。

登場人物

  • SPP (Serial Port Profile): Serial通信を可能にするBluetoothプロファイル。
  • SDP (Service Discovery Protocol): 使用可能プロファイルを通知するBluetoothプロファイル。
  • RFCOMM : SPPに関連したBluetoothプロファイル。

以下の二つを読めば0から設定できる、すごい。なので本稿では全体像と仕組みを示そうと思う。 Bluetoothを介した Windows <-> RPi シリアル通信 Raspberry Pi 2にBluetoothシリアル通信でデータ送受信してみた - カタカタブログ
シリアル通信に乗っかったRPiログイン Raspberry Pi 3にBluetoothでログインする - Qiita

シリアル通信からログインまで

rfcomm [ options ] < command > < dev >

Options
-r
Switch TTY into raw mode (doesn't work with "bind").

Commands
watch [channel] [cmd]
Listen on a specified RFCOMM channel for incoming connections.
If cmd is given, it will be executed as soon as a client connects.

sudo rfcomm -r watch 0 22 /sbin/agetty -L rfcomm0 115200 & 管理者権限において、rfcomm channel #x をwatchし、接続確立後ただちにボーレート115200にてログイン処理を行え

Man page of AGETTY
rfcomm(1): RFCOMM config utility - Linux man page

良いAPIを目指す形式たち

概念を削り込んでいったらここまで来てしまった

RESTful API
GraphQL
RPC
gRPC
browser Workers

プログラムから見た外部へのアクセス界面
自由な形式は混乱を産むから、賢いスタイル/形式が考案されてきた

RPC

ローカルに関数を呼ぶのと同様に、別の計算機に対し、関数名と引数を渡せば良い、という設計思想

// 通常の関数呼び出し
const local_result  = localfunc(arg1);
// RPCの理想像
const remote_result = remotefnc(arg2);
// RPCの実像
const rpc_result    = rpc(remotefnc, arg3);

理想像が使えたら最高である。しかし、現実には解くべき問題が無限にある。

funcのバージョンはどうやって指定する?暗示的?Arg1?
argの型制限は? named argは? 可変引数は?
通信プロトコルは? TCP+独自? HTTP?
遠隔計算機の指定方法は?
APIは各言語ごとに用意しなきゃいけないの?
ああああああああぁぁぁぁぁぁ

gRPC

より良いRPCを目指す形式。

RESTful

Webの世界で、よいClient-Server APIを目指したスタイル (規格ではない)
RPCのような手続き/関数中心の考え方ではなく、リソースが中心。
リソース/Entityがまず定義され、そこにURL/URIが割り当てられる。
リソースに対する操作がHTTP Methodsで規定され、アクセスする。
リソースがさき、レスポンスはあと。

GraphQL

Webの世界で、

name partial query one query cache monitoring
GraphQL built-in built-in
REST-Swagger with query (fields param) with good scheme

https://note.mu/konpyu/n/nc4fd122644a1

契約による設計

Client (Caller) とSupplier (Callee)
Obligationとbenefits

Design by Contract (契約による設計) はプログラミング技法のひとつ。
Eiffelには言語レベルで直接実装されている1 呼び出し側 (Client, メイン側) と呼び出され側 (Supplier, コルーチン・関数側) の間に保証されるべき条件を契約とみなし、契約を検証可能なコードとして記述する手法。
ClientとSupplierは義務と利益 (Obligation & Benefits) を持っているとみる。 Client目線では、義務を果たした状態でSupplierを呼び出せば利益が得られるという契約が結ばれている。
Supplier目線では、呼び出し側が常に正しい状態で呼び出してくれると保証されており、代わりに正しい利益をClientへ返す義務を負っている。
関数呼び出し時に満たすべき条件 (Precondition) コードによりClientの義務が確認されSupplierは利益を得る。関数が戻り値を返す際に満たすべき条件 (Postcondition) コードによりClientの利益が保証されSupplierは義務を果たすことになる。

The Power of Design by Contract™, Eiffel Software
ET: Design by Contract (tm), Assertions and Exceptions


  1. Eiffel directly implements the ideas of Design by Contract™ ref

定義域と値域 in プログラミング

どうやって担保するか

f: X -> Y
関数fは入力/引数 x ∈ 定義域X を取り、出力/返り値 y ∈ 定義域Y を返す
関数fはcallerによって呼び出される.
引数を渡すのはcallerであるから、正しい引数xを渡す責務はcallerにある.
正しい引数を渡された関数は y ∈ Yを返す責務がある.
プログラムの検証をするなら、X -> Y (関数の内容、振る舞い) の検証 + 呼び出し時 x ∈ Xの検証 (関数の使われ方) が必要

ポイントは

  • 定義域と値域を担保できるか
  • 値域-定義域ミスマッチを実行前に担保できるか
function step1(arg:int) => int  
function step2(arg:int) => int & >0  
function step3(arg:int&>0) => int & >20  
function setp4(arg:int&>10) => int  

// pattern A
step1(1)  // int => int
|> step2  // int => >0
|> step3  // >0  => >20
|> step4  // >10 => int
// properly work  

// pattern B
step1(1)  // int => int
|> step2  // int => >0
|> step4  // >10 => int
|> step3  // >0  => >20
// 2to4 (e.g. output==5), 4to3 (e.g. output==-5) cause mismatch

patternBは、潜在的に異常な動作をしうるコード
動的な検証をしようとしたら、異常な動作を引き起こさなきゃいけない。異常な動作を引き起こす (おそらくエッジケースの) 引数がわかっていたら、最初から異常動作しないようにコード書く.

アサーション

あらゆる制約を書ける。なので定義域/値域の完全な担保が可能 (なはず).
Design by ContractのPre/Post conditionはこれにほぼ相当する.
おそらくエディタによる補完等は効かない。
pipeの安全性確保はこちら側ですることになる。

型システム

各引数に型がつくのであって、定義域の元 (引数のセット) には型がつかない (引数群をクラスにすればできなくはない)。
定義域の完全な担保は難しい
structural subtypingを採用しているものなら、pipeの安全性を確保できる。最高に魅力的
型でDbCを徹底したいなら、interfaceを実装したクラスを作ってConstruct内でValidationさせれば一応できる。かなりハイカロリー (クラスの用意、2関数に強く結合しているが故の変更コスト)なので、コア部分で使うのが妥当かな.

テスト

値域はある程度担保できるけど、定義域外が入ってくるのを防ぐ方法はない.

ドキュメンテーション運用

人間は不完全な生き物である、残念ながら。

目的

関数に定義域外の引数が入らないようにする. 関数が値域外の返り値を返さないようにする.
型定義ではじく。assertionではじく。どっちもそれ用のテストはあった方がbetter
型およびassertionが動くことが確約されれば、関数が定義域外をはじく能力が確約される。
その上で、プログラム内で関数が呼ばれる際に渡される引数が正しいとどうやって保証するのか。
定義域外の入力がくると、確約された能力によってType ErrorかAssertion Errorが発生しプログラムが停止する。だからプロダクション環境に入れる前に引数の正しさを保証する必要がある。
型を利用する場合は、引数の型を確認すればいいだけ。
Assertionを利用しようとした場合、「引数を生成した関数の返り値assertion条件 ⊂ 引数受け入れassertion条件」を目視 (あるいは自動検証) で確認しなければいけなくなる。あれ、目視あるいは自動検証って静的検査なのでは?もうほぼ静的型検査と変わらないのでは?
動的に検査するのであれば、引数生成関数にじゃんじゃかinputしてテストするしかない。さて2関数をまたぐテストケースはいくつどんなバリエーションで作ればいいのか…

検証方法

動的検証の場合、値に対する振る舞いを検査することになる.
具体的な値でなく変数の特性で検証すれば、関数呼び出しの正当性も検証できる.

動的な手法は具体的な値に関する何か (値の内容、値の型) を検査することになる?
定義域/値域は具体的な値というより変数の特性だから、型みたいな変数の特性を示すものでhandleしないと検証できない (総当たりが不可能なほとんどの場合で)

qiita.com

手法

アサーション/validation
静的型チェック 動的型チェック

Property-based testing

入力に対する制約

一般に入力バリデーションと呼ばれるもの。

対象は関数からフォームまで色々広く

プログラムは (明示的・暗示的に) 入力に想定範囲を持つ

プログラムを書く際、入力には範囲が想定されている。
argAは文字列だとか、英数字だけだとか、intだとか、非ゼロだとか.
指定していなくても、関数内のコードでは入力はこの辺りだと暗示的に考えながら書いていることが多い.
想定外の領域が正しい振る舞いをするか否かは、神のみぞ知る (保証されない).
正しく振る舞って欲しいのなら、入力は想定範囲内に収められていなければならない。

入力に制約を設けるメリット

想定範囲外の入力が引き起こす正しくない振る舞いが原理上起きなくなる.

セキュリティの観点から見れば、安全が確保されやすくなる。
good codingの観点からみれば、codingの大半を占めるDebugが減る.
behavior driven developmentの観点からみれば、関数の定義域が明確になるので振る舞い設計が明確になる.
テストの観点からみれば、テスト範囲が限定されるのでテスト作成不可が減り実質のカバレッジも上がる.

入力に対する制約の実現方法

  • 型: ざくっりした入力の制約
    • 入力組み合わせに対する制約は型で記述するのが手間 (な気がする)
  • 入力バリデーション: 完全に記述が可能

強く関連するトピック

  • セキュアプログラミング(防衛的プログラミング): 安全性の観点から。セキュアプログラミングの一方法論としての入力バリデーション
  • DbC, 契約プログラミング: バグ抑制の観点から

word

疑問点

静的に評価できるのか?
関数をpipeしているときにpipeの出入力で範囲がミスマッチ起こしていないか確認できないか?

実用

JS

  1. まず型を導入してみる (TypeScript etc)
  2. 関数の頭にasset入れて端から検証 (ドキュメンテーションがつらみ)
  3. DbC補助ライブラリの導入

qiita.com

# DbCで入出力をきっちりして、きっちりして…?
動的バリデーションをずっとかけておけば、バグった時にちゃんとassertはしてくれる。
全モジュールで入出力バリデーションしとけば、安全。

独自型を書くのと何が違うのだろうか.

依存型

myuon.github.io

オブジェクト型にして、validationかけておけば事実上は制限付き型に出来はする

型とvalidationを比べてメリットデメリット

documentation: 型のほうが色々充実しているイメージ

UQモバイル データ繰り越し: 増量分は含まれないよ

データ繰り越し

一言でいうと: 余ったギガを、ある程度繰り越せる
正確にいうと: 通信容量の基本分が余った場合、それを繰り越せる (上限は基本分1ヶ月)
基本データ通信容量は S: 2GB, M: 6GB, L: 14GB ref..

ポイント

繰り越しと、データチャージの有効期限は別物。合わせると理解不能になるよ。

繰り越し

繰り越しは、データチャージを一切無視して基本プランの上限に達さなかった場合に繰り越しが発生するということ。
プラン変更後の基本容量で繰り越し上限が決まるので、Mで貯めてSに引き継ごうとしても2GBしか引き継げない (2+1+2 = 5GBなら充分、という考え方も)
また繰り越し分の繰り越し、的なことはできない。有効期限は翌月のみ。

基本データ通信容量の残量は、翌月に適用されるプランの基本データ通信容量と同容量まで翌月に繰越できます。
容量消費は、繰り越し分>基本データ容量>追加購入データ容量の順番に行われます。
データチャージにより追加購入いただいたデータ容量は、繰り越しの対象外となります。
データ通信の便利機能について|【公式】UQ mobile|UQコミュニケーションズ

繰り越したデータ容量に有効期限はありますか? | よくあるご質問|【公式】UQ mobile|UQコミュニケーションズ

データチャージの有効期限

増量オプション含むデータチャージは、もともと3ヶ月の有効期限を持っている。
増量オプションはデータチャージ1回分を割り引いてくれるサービス。

チャージしたデータ容量が残っている状態で追加購入した場合、全てのチャージ分の有効期限が最終チャージ(購入)日より90日後に上書きされます。
データ通信の便利機能について|【公式】UQ mobile|UQコミュニケーションズ